noncomputable def SobolevHilbert.japaneseBracket {E : Type u_1} [NormedAddCommGroup E] (ξ : E) : ℝ

The Japanese bracket ⟨ξ⟩ := sqrt(1 + ‖ξ‖²) used as a smooth comparison weight.

noncomputable def SobolevHilbert.sobolevWeight {E : Type u_1} [NormedAddCommGroup E] (m : ℝ) (ξ : E) : ℝ

The Sobolev weight (1 + ‖ξ‖²)^m, the symbol used to define H^m via the Fourier transform.

theorem SobolevHilbert.japaneseBracket_pos {E : Type u_1} [NormedAddCommGroup E] (ξ : E) : 0 < japaneseBracket ξ

The Japanese bracket is strictly positive.

theorem SobolevHilbert.sobolevWeight_pos {E : Type u_1} [NormedAddCommGroup E] (m : ℝ) (ξ : E) : 0 < sobolevWeight m ξ

The Sobolev weight is strictly positive for every real exponent.

theorem SobolevHilbert.sobolevSpace_contDiff {n m : ℕ} (u : SobolevEmbedding.SobolevSpace n m) (j : ℕ) (hj : j ≤ m) : ContDiff ℝ (↑↑j) u.toFun

Elements of SobolevSpace n m are j-times continuously differentiable for any j ≤ m.

theorem SobolevHilbert.sobolevSpace_add_memLp {n m : ℕ} (u v : SobolevEmbedding.SobolevSpace n m) (j : ℕ) (hj : j ≤ m) : MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ (Fin n)) => iteratedFDeriv ℝ j (u.toFun + v.toFun) x) 2 MeasureTheory.volume

The j-th iterated Fréchet derivative of the sum of two SobolevSpace n m elements is in L^2.

theorem SobolevHilbert.l2_triangle_range (k : ℕ) (a b : ℕ → ℝ) : √(∑ j ∈ Finset.range k, (a j + b j) ^ 2) ≤ √(∑ j ∈ Finset.range k, a j ^ 2) + √(∑ j ∈ Finset.range k, b j ^ 2)

The triangle inequality for the ℓ^2 norm of finite sequences indexed by Finset.range k.

theorem SobolevHilbert.sqrt_sum_sq_mono {k : ℕ} {c d : ℕ → ℝ} (hc : ∀ j ∈ Finset.range k, 0 ≤ c j) (hle : ∀ j ∈ Finset.range k, c j ≤ d j) : √(∑ j ∈ Finset.range k, c j ^ 2) ≤ √(∑ j ∈ Finset.range k, d j ^ 2)

Monotonicity of sqrt (∑ c j ^ 2) in pointwise nonnegative bounds c j ≤ d j.

theorem SobolevHilbert.sobolevSpace_norm_triangle {n m : ℕ} (u v : SobolevEmbedding.SobolevSpace n m) : √(∑ j ∈ Finset.range (m + 1), (MeasureTheory.eLpNorm (fun (x : EuclideanSpace ℝ (Fin n)) => iteratedFDeriv ℝ j (u.toFun + v.toFun) x) 2 MeasureTheory.volume).toReal ^ 2) ≤ √(∑ j ∈ Finset.range (m + 1), (MeasureTheory.eLpNorm (fun (x : EuclideanSpace ℝ (Fin n)) => iteratedFDeriv ℝ j u.toFun x) 2 MeasureTheory.volume).toReal ^ 2) + √(∑ j ∈ Finset.range (m + 1), (MeasureTheory.eLpNorm (fun (x : EuclideanSpace ℝ (Fin n)) => iteratedFDeriv ℝ j v.toFun x) 2 MeasureTheory.volume).toReal ^ 2)

Triangle inequality for the Sobolev H^m norm on SobolevSpace n m.

theorem SobolevHilbert.sobolevSpace_ae_eq_zero_imp_eq_zero {n m : ℕ} (u : SobolevEmbedding.SobolevSpace n m) (hae : u.toFun =ᵐ[MeasureTheory.volume] 0) : u.toFun = 0

A continuous Sobolev function that vanishes almost everywhere vanishes identically.

theorem SobolevHilbert.sobolevSpace_norm_separation {n m : ℕ} (u : SobolevEmbedding.SobolevSpace n m) (h : ∀ j ≤ m, (MeasureTheory.eLpNorm (fun (x : EuclideanSpace ℝ (Fin n)) => iteratedFDeriv ℝ j u.toFun x) 2 MeasureTheory.volume).toReal = 0) : u.toFun = 0

Separation property: if every Sobolev semi-norm of u vanishes, then the underlying function is zero.

theorem SobolevHilbert.SobolevEmbedding.SobolevSpace.ext' {n m : ℕ} {u v : SobolevEmbedding.SobolevSpace n m} (h : u.toFun = v.toFun) : u = v

Extensionality for SobolevSpace n m: equality is determined by the underlying function.

theorem SobolevHilbert.SobolevEmbedding.SobolevSpace.ext'_iff {n m : ℕ} {u v : SobolevEmbedding.SobolevSpace n m} : u = v ↔ u.toFun = v.toFun

@[implicit_reducible]

instance SobolevHilbert.sobolevSpaceZero (n m : ℕ) : Zero (SobolevEmbedding.SobolevSpace n m)

The zero element of SobolevSpace n m.

@[implicit_reducible]

instance SobolevHilbert.sobolevSpaceNeg (n m : ℕ) : Neg (SobolevEmbedding.SobolevSpace n m)

Negation on SobolevSpace n m, obtained by negating the underlying function.

@[implicit_reducible]

instance SobolevHilbert.sobolevSpaceAdd (n m : ℕ) : Add (SobolevEmbedding.SobolevSpace n m)

Addition on SobolevSpace n m, obtained pointwise on the underlying functions.

@[simp]

theorem SobolevHilbert.sobolevSpace_add_toFun {n m : ℕ} (u v : SobolevEmbedding.SobolevSpace n m) : (u + v).toFun = u.toFun + v.toFun

Underlying-function form of addition on SobolevSpace n m.

@[simp]

theorem SobolevHilbert.sobolevSpace_neg_toFun {n m : ℕ} (u : SobolevEmbedding.SobolevSpace n m) : (-u).toFun = -u.toFun

Underlying-function form of negation on SobolevSpace n m.

@[simp]

theorem SobolevHilbert.sobolevSpace_zero_toFun (n m : ℕ) : SobolevEmbedding.SobolevSpace.toFun 0 = 0

The underlying function of the zero element is the zero function.

@[implicit_reducible]

instance SobolevHilbert.sobolevSpace_addCommGroup' (n m : ℕ) : AddCommGroup (SobolevEmbedding.SobolevSpace n m)

The additive commutative group structure on SobolevSpace n m.

noncomputable def SobolevHilbert.sobolevNorm {n m : ℕ} (u : SobolevEmbedding.SobolevSpace n m) : ℝ

The Sobolev H^m norm of u: the ℓ^2 sum of the L^2 norms of all iterated derivatives up to order m.

theorem SobolevHilbert.sobolevNorm_neg' {n m : ℕ} (u : SobolevEmbedding.SobolevSpace n m) : sobolevNorm (-u) = sobolevNorm u

The Sobolev norm is invariant under negation.

theorem SobolevHilbert.sobolevNorm_zero' (n m : ℕ) : sobolevNorm 0 = 0

The Sobolev norm of the zero element is zero.

theorem SobolevHilbert.sobolevNorm_eq_zero_iff {n m : ℕ} (u : SobolevEmbedding.SobolevSpace n m) (h : sobolevNorm u = 0) : u = 0

If the Sobolev norm of u is zero, then u = 0.

@[reducible, inline]

noncomputable abbrev SobolevHilbert.sobolevSpace_nacg (n m : ℕ) : NormedAddCommGroup (SobolevEmbedding.SobolevSpace n m)

The normed additive commutative group structure on SobolevSpace n m from the Sobolev norm.

theorem SobolevHilbert.sobolevSpace_smul_memLp {n m : ℕ} (c : ℂ) (u : SobolevEmbedding.SobolevSpace n m) (j : ℕ) (hj : j ≤ m) : MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ (Fin n)) => iteratedFDeriv ℝ j (c • u.toFun) x) 2 MeasureTheory.volume

The j-th iterated derivative of c • u is in L^2 for scalar c and u ∈ SobolevSpace n m.

@[implicit_reducible]

instance SobolevHilbert.sobolevSpaceSMul (n m : ℕ) : SMul ℂ (SobolevEmbedding.SobolevSpace n m)

The scalar multiplication of ℂ on SobolevSpace n m.

@[simp]

theorem SobolevHilbert.sobolevSpace_smul_toFun {n m : ℕ} (c : ℂ) (u : SobolevEmbedding.SobolevSpace n m) : (c • u).toFun = c • u.toFun

Underlying-function form of scalar multiplication on SobolevSpace n m.

@[implicit_reducible]

instance SobolevHilbert.sobolevSpace_module' (n m : ℕ) : Module ℂ (SobolevEmbedding.SobolevSpace n m)

The ℂ-module structure on SobolevSpace n m.

theorem SobolevHilbert.sobolevSpace_norm_smul_le {n m : ℕ} (c : ℂ) (u : SobolevEmbedding.SobolevSpace n m) : ‖c • u‖ ≤ ‖c‖ * ‖u‖

The Sobolev norm is homogeneous (bounded by) ‖c‖ * ‖u‖ under scalar multiplication.

@[implicit_reducible]

instance SobolevHilbert.sobolevSpace_normedSpace' (n m : ℕ) : NormedSpace ℂ (SobolevEmbedding.SobolevSpace n m)

The complex NormedSpace structure on SobolevSpace n m.

noncomputable def SobolevHilbert.sobolevFourierEquiv (n m : ℕ) : SobolevEmbedding.SobolevSpace n m ≃ ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

The Fourier-side identification of SobolevSpace n m with L^2 (as a bare equivalence).

theorem SobolevHilbert.sobolevFourierEquiv_isometry (n m : ℕ) : Isometry (sobolevFourierEquiv n m).toFun

The Fourier-side equivalence sobolevFourierEquiv is an isometry between the Sobolev norm and the L^2 norm.

noncomputable def SobolevHilbert.sobolevFourierIsometry (n m : ℕ) : SobolevEmbedding.SobolevSpace n m ≃ᵢ ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

Packaging sobolevFourierEquiv and its isometry property as an IsometryEquiv.

theorem SobolevHilbert.sobolevFourierEquiv_map_zero (n m : ℕ) : (sobolevFourierEquiv n m) 0 = 0

The Fourier-side equivalence sends 0 to 0.

theorem SobolevHilbert.sobolevFourierIsometry_map_zero (n m : ℕ) : (sobolevFourierIsometry n m) 0 = 0

The Fourier-side isometry sends 0 to 0.

theorem SobolevHilbert.sobolevFourierEquiv_map_I_smul (n m : ℕ) (u : SobolevEmbedding.SobolevSpace n m) : (sobolevFourierEquiv n m) (Complex.I • u) = Complex.I • (sobolevFourierEquiv n m) u

The Fourier-side equivalence commutes with multiplication by Complex.I.

theorem SobolevHilbert.sobolevFourierIsometry_map_I_smul (n m : ℕ) (u : SobolevEmbedding.SobolevSpace n m) : (sobolevFourierIsometry n m) (Complex.I • u) = Complex.I • (sobolevFourierIsometry n m) u

The Fourier-side isometry commutes with multiplication by Complex.I.

noncomputable def SobolevHilbert.sobolevFourierLinearIsometry (n m : ℕ) : SobolevEmbedding.SobolevSpace n m ≃ₗᵢ[ℝ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

The Fourier-side ℝ-linear isometric equivalence SobolevSpace n m ≃ₗᵢ[ℝ] Lp ℂ 2.

@[simp]

theorem SobolevHilbert.sobolevFourierLinearIsometry_apply (n m : ℕ) (u : SobolevEmbedding.SobolevSpace n m) : (sobolevFourierLinearIsometry n m) u = (sobolevFourierIsometry n m) u

The ℝ-linear isometry agrees pointwise with the bare isometry.

theorem SobolevHilbert.sobolevFourierLinearIsometry_map_I_smul (n m : ℕ) (u : SobolevEmbedding.SobolevSpace n m) : (sobolevFourierLinearIsometry n m) (Complex.I • u) = Complex.I • (sobolevFourierLinearIsometry n m) u

The ℝ-linear Fourier isometry commutes with multiplication by Complex.I.

theorem SobolevHilbert.sobolevFourierLinearIsometry_map_smul (n m : ℕ) (c : ℂ) (u : SobolevEmbedding.SobolevSpace n m) : (sobolevFourierLinearIsometry n m) (c • u) = c • (sobolevFourierLinearIsometry n m) u

The ℝ-linear Fourier isometry is also ℂ-linear: it commutes with multiplication by any complex scalar.

noncomputable def SobolevHilbert.sobolevInner {n m : ℕ} (u v : SobolevEmbedding.SobolevSpace n m) : ℂ

The Sobolev inner product on SobolevSpace n m, transported from the L^2 inner product through the Fourier isometry.

@[implicit_reducible]

noncomputable instance SobolevHilbert.sobolevSpace_inner' (n m : ℕ) : Inner ℂ (SobolevEmbedding.SobolevSpace n m)

The complex Inner instance on SobolevSpace n m given by sobolevInner.

theorem SobolevHilbert.sobolevInner_norm_sq {n m : ℕ} (u : SobolevEmbedding.SobolevSpace n m) : ‖u‖ ^ 2 = (sobolevInner u u).re

The Sobolev norm squared equals the real part of ⟨u, u⟩.

theorem SobolevHilbert.sobolevInner_conj_symm {n m : ℕ} (u v : SobolevEmbedding.SobolevSpace n m) : (starRingEnd ℂ) (sobolevInner v u) = sobolevInner u v

Conjugate symmetry: conj ⟨v, u⟩ = ⟨u, v⟩.

theorem SobolevHilbert.sobolevInner_add_left {n m : ℕ} (u v w : SobolevEmbedding.SobolevSpace n m) : sobolevInner (u + v) w = sobolevInner u w + sobolevInner v w

Additivity of the inner product in the left argument.

theorem SobolevHilbert.sobolevInner_smul_left {n m : ℕ} (u v : SobolevEmbedding.SobolevSpace n m) (c : ℂ) : sobolevInner (c • u) v = (starRingEnd ℂ) c * sobolevInner u v

Conjugate-linearity in the left argument: ⟨c • u, v⟩ = conj c * ⟨u, v⟩.

@[reducible, inline]

noncomputable abbrev SobolevHilbert.sobolevSpace_innerProductSpace (n m : ℕ) : InnerProductSpace ℂ (SobolevEmbedding.SobolevSpace n m)

The complex inner product space structure on SobolevSpace n m.

theorem SobolevHilbert.sobolevSpace_completeSpace (n m : ℕ) : CompleteSpace (SobolevEmbedding.SobolevSpace n m)

Completeness of SobolevSpace n m, inherited via the Fourier isometry with L^2.

noncomputable def SobolevHilbert.sobolevSpace_toL2 (n m : ℕ) [NormedAddCommGroup (SobolevEmbedding.SobolevSpace n m)] (u : SobolevEmbedding.SobolevSpace n m) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

The map sending u ∈ SobolevSpace n m to its image in L^2 via the Fourier isometry.

theorem SobolevHilbert.sobolevSpace_toL2_norm_sub (n m : ℕ) (u v : SobolevEmbedding.SobolevSpace n m) : ‖u - v‖ = ‖sobolevSpace_toL2 n m u - sobolevSpace_toL2 n m v‖

Isometric property of sobolevSpace_toL2 on differences.

theorem SobolevHilbert.schwartz_iteratedFDeriv_memLp {n m : ℕ} (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (j : ℕ) (hj : j ≤ m) : MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ (Fin n)) => iteratedFDeriv ℝ j (⇑φ) x) 2 MeasureTheory.volume

For any Schwartz function φ and j ≤ m, the iterated derivative of φ is in L^2.

noncomputable def SobolevHilbert.schwartzToSobolev (n m : ℕ) (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) : SobolevEmbedding.SobolevSpace n m

Promote a Schwartz function to an element of SobolevSpace n m.

@[simp]

theorem SobolevHilbert.schwartzToSobolev_toFun (n m : ℕ) (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) : (schwartzToSobolev n m φ).toFun = ⇑φ

The underlying function of schwartzToSobolev n m φ is ⇑φ.

theorem SobolevHilbert.sobolevFourierEquiv_schwartz (n m : ℕ) (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) : (sobolevFourierEquiv n m) (schwartzToSobolev n m φ) = φ.toLp 2 MeasureTheory.volume

The Fourier-side equivalence sends the embedded Schwartz function to its L^2-class.

theorem SobolevHilbert.sobolevFourierIsometry_schwartz_toLp (n m : ℕ) [NormedAddCommGroup (SobolevEmbedding.SobolevSpace n m)] (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) : sobolevSpace_toL2 n m (schwartzToSobolev n m φ) = φ.toLp 2 MeasureTheory.volume

The Fourier isometry sends the embedded Schwartz function to its L^2-class.

theorem SobolevHilbert.sobolevSpace_schwartz_toLp (n m : ℕ) [NormedAddCommGroup (SobolevEmbedding.SobolevSpace n m)] (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) : ∃ (v : SobolevEmbedding.SobolevSpace n m), v.toFun = ⇑φ ∧ sobolevSpace_toL2 n m v = φ.toLp 2 MeasureTheory.volume

Existence of a Sobolev representative whose underlying function is ⇑φ and whose L^2 image is SchwartzMap.toLp φ.

theorem SobolevHilbert.proposition_9_8 (n : ℕ) (m : ℝ) : (∃ (Φ : SobolevSpace.Hs n m ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)), DenseRange (⇑Φ.symm ∘ ⇑(SchwartzMap.toLpCLM ℝ ℂ 2 MeasureTheory.volume))) ∧ Nonempty (SobolevSpace.Hs n (-m) ≃ₗᵢ⋆[ℂ] SobolevSpace.Hs n m →L[ℂ] ℂ)

Melrose Proposition 9.8: H^m(ℝⁿ) is a Hilbert space (Fourier-side isomorphic to L²), and its dual is H^{-m}(ℝⁿ).