Sobolev embedding for general smooth fields on R³, without Schwartz assumptions.

noncomputable def EulerSmoothSobolev.pureDerivative {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (d n : ℕ) (v : EulerSobolev.Domain d) (f : SchwartzMap (EulerSobolev.Domain d) F) : SchwartzMap (EulerSobolev.Domain d) F

Repeated directional derivatives of a vector-valued Schwartz function.

Equations

• EulerSmoothSobolev.pureDerivative d n v f = EulerSobolev.schwartzIteratedDerivative (fun (x : Fin n) => v) f

theorem EulerSmoothSobolev.fourier_pureDerivative_norm {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (d n : ℕ) (v : EulerSobolev.Domain d) (f : SchwartzMap (EulerSobolev.Domain d) F) (ξ : EulerSobolev.Domain d) : ‖(EulerSobolev.schwartzFourier (pureDerivative d n v f)) ξ‖ = (2 * Real.pi) ^ n * ‖inner ℝ ξ v‖ ^ n * ‖(EulerSobolev.schwartzFourier f) ξ‖

noncomputable def EulerSmoothSobolev.normLp {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (d : ℕ) (f : SchwartzMap (EulerSobolev.Domain d) F) : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)

The pointwise norm of a Schwartz function, represented in the real L² space.

Equations

• EulerSmoothSobolev.normLp d f = MeasureTheory.MemLp.toLp (fun (x : EulerSobolev.Domain d) => ‖f x‖) ⋯

theorem EulerSmoothSobolev.norm_normLp {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (d : ℕ) (f : SchwartzMap (EulerSobolev.Domain d) F) : ‖normLp d f‖ = ‖f.toLp 2 MeasureTheory.volume‖

theorem EulerSmoothSobolev.coe_normLp {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (d : ℕ) (f : SchwartzMap (EulerSobolev.Domain d) F) : ↑↑(normLp d f) =ᵐ[MeasureTheory.volume] fun (x : EulerSobolev.Domain d) => ‖f x‖

theorem EulerSmoothSobolev.normLp_le_sum {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] {ι : Type u_2} [Fintype ι] (d : ℕ) (f : SchwartzMap (EulerSobolev.Domain d) F) (g : ι → SchwartzMap (EulerSobolev.Domain d) F) (C : ℝ) (hC : 0 ≤ C) (h : ∀ (x : EulerSobolev.Domain d), ‖f x‖ ≤ C * ∑ i : ι, ‖(g i) x‖) : ‖f.toLp 2 MeasureTheory.volume‖ ≤ C * ∑ i : ι, ‖(g i).toLp 2 MeasureTheory.volume‖

theorem EulerSmoothSobolev.sobolevNorm_two_le_pure_derivatives {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] (d : ℕ) (f : SchwartzMap (EulerSobolev.Domain d) F) : EulerSobolev.sobolevNorm d 2 f ≤ 1 * (‖f.toLp 2 MeasureTheory.volume‖ + (2 * Real.pi) ^ (-2) * ∑ i : Fin d, ‖(pureDerivative d 2 (EuclideanSpace.single i 1) f).toLp 2 MeasureTheory.volume‖)

theorem EulerSmoothSobolev.pointwise_le_L2_second_derivatives {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] (f : SchwartzMap (EulerSobolev.Domain 3) F) (x : EulerSobolev.Domain 3) : ‖f x‖ ≤ EulerSobolev.embeddingConstant 3 2 pointwise_le_L2_second_derivatives._proof_1 * (‖f.toLp 2 MeasureTheory.volume‖ + (2 * Real.pi) ^ (-2) * ∑ i : Fin 3, ‖(pureDerivative 3 2 (EuclideanSpace.single i 1) f).toLp 2 MeasureTheory.volume‖)

The sharp three-dimensional H² pointwise bound in terms of actual second derivatives.

noncomputable def EulerSmoothSobolev.tensorSobolevNorm {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (s : ℕ) (f : EulerSobolev.Domain 3 → F) : ℝ

The sum of the actual L² norms of Fréchet derivatives through order s.

Equations

• EulerSmoothSobolev.tensorSobolevNorm s f = ∑ j ∈ Finset.range (s + 1), (MeasureTheory.eLpNorm (iteratedFDeriv ℝ j f) 2 MeasureTheory.volume).toReal

theorem EulerSmoothSobolev.tensorSobolevNorm_nonneg {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (s : ℕ) (f : EulerSobolev.Domain 3 → F) : 0 ≤ tensorSobolevNorm s f

theorem EulerSmoothSobolev.tensorSobolevNorm_mono {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] {s t : ℕ} (hst : s ≤ t) (f : EulerSobolev.Domain 3 → F) : tensorSobolevNorm s f ≤ tensorSobolevNorm t f

noncomputable def EulerSmoothSobolev.derivativeMagnitude {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (s : ℕ) (f : EulerSobolev.Domain 3 → F) (x : EulerSobolev.Domain 3) : ℝ

Sum of the pointwise norms of all derivatives through a fixed order.

Equations

• EulerSmoothSobolev.derivativeMagnitude s f x = ∑ j ∈ Finset.range (s + 1), ‖iteratedFDeriv ℝ j f x‖

theorem EulerSmoothSobolev.derivativeMagnitude_nonneg {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (s : ℕ) (f : EulerSobolev.Domain 3 → F) (x : EulerSobolev.Domain 3) : 0 ≤ derivativeMagnitude s f x

theorem EulerSmoothSobolev.derivativeMagnitude_memLp {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (s : ℕ) (f : EulerSobolev.Domain 3 → F) (hfL2 : ∀ j ≤ s, MeasureTheory.MemLp (iteratedFDeriv ℝ j f) 2 MeasureTheory.volume) : MeasureTheory.MemLp (derivativeMagnitude s f) 2 MeasureTheory.volume

theorem EulerSmoothSobolev.derivativeMagnitude_L2_le {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (s : ℕ) (f : EulerSobolev.Domain 3 → F) (hfL2 : ∀ j ≤ s, MeasureTheory.MemLp (iteratedFDeriv ℝ j f) 2 MeasureTheory.volume) : ‖MeasureTheory.MemLp.toLp (derivativeMagnitude s f) ⋯‖ ≤ tensorSobolevNorm s f

noncomputable def EulerSmoothSobolev.unitBump : ContDiffBump 0

A fixed bump equal to one near zero, independent of the function being estimated.

Equations

• EulerSmoothSobolev.unitBump = { rIn := 1, rOut := 2, rIn_pos := EulerSmoothSobolev.unitBump._proof_1, rIn_lt_rOut := EulerSmoothSobolev.unitBump._proof_2 }

noncomputable def EulerSmoothSobolev.unitBumpSchwartz : SchwartzMap (EulerSobolev.Domain 3) ℝ

The same fixed bump as a Schwartz function.

Equations

• EulerSmoothSobolev.unitBumpSchwartz = EulerSmoothSobolev.unitBumpSchwartz._proof_2.toSchwartzMap EulerSmoothSobolev.unitBumpSchwartz._proof_3

noncomputable def EulerSmoothSobolev.unitBumpBound (j : ℕ) : NNReal

A finite derivative bound for the fixed bump.

Equations

• EulerSmoothSobolev.unitBumpBound j = ⟨(SchwartzMap.seminorm ℝ 0 j) EulerSmoothSobolev.unitBumpSchwartz, ⋯⟩

noncomputable def EulerSmoothSobolev.unitBumpCoefficient (n : ℕ) : NNReal

The finite Leibniz coefficient for localizing an order n derivative.

Equations

• EulerSmoothSobolev.unitBumpCoefficient n = ∑ j ∈ Finset.range (n + 1), ↑(n.choose j) * EulerSmoothSobolev.unitBumpBound j

noncomputable def EulerSmoothSobolev.localize {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (f : EulerSobolev.Domain 3 → F) (hf : ContDiff ℝ (↑⊤) f) (x : EulerSobolev.Domain 3) : SchwartzMap (EulerSobolev.Domain 3) F

An actual smooth compact localization of an arbitrary smooth function about x.

Equations

• EulerSmoothSobolev.localize f hf x = ⋯.toSchwartzMap ⋯

@[simp]

theorem EulerSmoothSobolev.localize_apply {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (f : EulerSobolev.Domain 3 → F) (hf : ContDiff ℝ (↑⊤) f) (x z : EulerSobolev.Domain 3) : (localize f hf x) z = ↑unitBump z • f (x + z)

theorem EulerSmoothSobolev.localize_zero {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (f : EulerSobolev.Domain 3 → F) (hf : ContDiff ℝ (↑⊤) f) (x : EulerSobolev.Domain 3) : (localize f hf x) 0 = f x

theorem EulerSmoothSobolev.localize_tensor_bound {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (n : ℕ) (f : EulerSobolev.Domain 3 → F) (hf : ContDiff ℝ (↑⊤) f) (x z : EulerSobolev.Domain 3) : ‖iteratedFDeriv ℝ n (⇑(localize f hf x)) z‖ ≤ ↑(unitBumpCoefficient n) * derivativeMagnitude n f (x + z)

Localization obeys the actual tensor Leibniz estimate.

theorem EulerSmoothSobolev.localize_pureDerivative_L2_le {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (n : ℕ) (i : Fin 3) (f : EulerSobolev.Domain 3 → F) (hf : ContDiff ℝ (↑⊤) f) (hfL2 : ∀ j ≤ n, MeasureTheory.MemLp (iteratedFDeriv ℝ j f) 2 MeasureTheory.volume) (x : EulerSobolev.Domain 3) : ‖(pureDerivative 3 n (EuclideanSpace.single i 1) (localize f hf x)).toLp 2 MeasureTheory.volume‖ ≤ ↑(unitBumpCoefficient n) * tensorSobolevNorm n f

Each localized pure derivative is controlled by the global physical Sobolev norm.

noncomputable def EulerSmoothSobolev.smoothEmbeddingConstant : ℝ

A fixed finite three-dimensional H² embedding constant.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerSmoothSobolev.smoothEmbeddingConstant_nonneg : 0 ≤ smoothEmbeddingConstant

theorem EulerSmoothSobolev.smooth_pointwise_le_H2 {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] (f : EulerSobolev.Domain 3 → F) (hf : ContDiff ℝ (↑⊤) f) (hfL2 : ∀ j ≤ 2, MeasureTheory.MemLp (iteratedFDeriv ℝ j f) 2 MeasureTheory.volume) (x : EulerSobolev.Domain 3) : ‖f x‖ ≤ smoothEmbeddingConstant * tensorSobolevNorm 2 f

Genuine H² to L∞ embedding for every smooth Hilbert-valued function on R³.

noncomputable def EulerSmoothSobolev.coordinateDerivative {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (i : Fin 3) (f : EulerSobolev.Domain 3 → F) : EulerSobolev.Domain 3 → F

The actual derivative in one Euclidean coordinate direction.

Equations

• EulerSmoothSobolev.coordinateDerivative i f x = (fderiv ℝ f x) (EuclideanSpace.single i 1)

theorem EulerSmoothSobolev.coordinateDerivative_smooth {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (i : Fin 3) (f : EulerSobolev.Domain 3 → F) (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (coordinateDerivative i f)

theorem EulerSmoothSobolev.coordinateDerivative_tensor_bound {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (j : ℕ) (i : Fin 3) (f : EulerSobolev.Domain 3 → F) (hf : ContDiff ℝ (↑⊤) f) (x : EulerSobolev.Domain 3) : ‖iteratedFDeriv ℝ j (coordinateDerivative i f) x‖ ≤ ‖iteratedFDeriv ℝ (j + 1) f x‖

theorem EulerSmoothSobolev.coordinateDerivative_tensor_memLp {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] {j : ℕ} (i : Fin 3) (f : EulerSobolev.Domain 3 → F) (hf : ContDiff ℝ (↑⊤) f) (hfL2 : MeasureTheory.MemLp (iteratedFDeriv ℝ (j + 1) f) 2 MeasureTheory.volume) : MeasureTheory.MemLp (iteratedFDeriv ℝ j (coordinateDerivative i f)) 2 MeasureTheory.volume

theorem EulerSmoothSobolev.coordinateDerivative_H2_le_H3 {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (i : Fin 3) (f : EulerSobolev.Domain 3 → F) (hf : ContDiff ℝ (↑⊤) f) (hfL2 : ∀ j ≤ 3, MeasureTheory.MemLp (iteratedFDeriv ℝ j f) 2 MeasureTheory.volume) : tensorSobolevNorm 2 (coordinateDerivative i f) ≤ 3 * tensorSobolevNorm 3 f

theorem EulerSmoothSobolev.linear_norm_le_coordinate_sum {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (A : EulerSobolev.Domain 3 →L[ℝ] F) : ‖A‖ ≤ ∑ i : Fin 3, ‖A (EuclideanSpace.single i 1)‖

A linear map is controlled by the sum of its values on the coordinate basis.

theorem EulerSmoothSobolev.smooth_fderiv_le_H3 {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] (f : EulerSobolev.Domain 3 → F) (hf : ContDiff ℝ (↑⊤) f) (hfL2 : ∀ j ≤ 3, MeasureTheory.MemLp (iteratedFDeriv ℝ j f) 2 MeasureTheory.volume) (x : EulerSobolev.Domain 3) : ‖fderiv ℝ f x‖ ≤ 9 * smoothEmbeddingConstant * tensorSobolevNorm 3 f

The exact regularity needed in the limiting Euler contradiction: H³ controls the C¹ derivative.

noncomputable def EulerSmoothSobolev.realTensorSobolevNorm (q s : ℕ) (f : EulerSobolev.Domain 3 → EulerSobolev.Domain q) : ℝ

The physical tensor Sobolev norm for real Euclidean vector fields.

Equations

• EulerSmoothSobolev.realTensorSobolevNorm q s f = ∑ j ∈ Finset.range (s + 1), (MeasureTheory.eLpNorm (iteratedFDeriv ℝ j f) 2 MeasureTheory.volume).toReal

theorem EulerSmoothSobolev.complexification_tensor_norm (q j : ℕ) (f : EulerSobolev.Domain 3 → EulerSobolev.Domain q) (hf : ContDiff ℝ (↑⊤) f) (x : EulerSobolev.Domain 3) : ‖iteratedFDeriv ℝ j (⇑(EulerSobolev.complexify q) ∘ f) x‖ = ‖iteratedFDeriv ℝ j f x‖

theorem EulerSmoothSobolev.complexification_tensor_memLp (q j : ℕ) (f : EulerSobolev.Domain 3 → EulerSobolev.Domain q) (hf : ContDiff ℝ (↑⊤) f) (hfL2 : MeasureTheory.MemLp (iteratedFDeriv ℝ j f) 2 MeasureTheory.volume) : MeasureTheory.MemLp (iteratedFDeriv ℝ j (⇑(EulerSobolev.complexify q) ∘ f)) 2 MeasureTheory.volume

theorem EulerSmoothSobolev.complexification_sobolevNorm (q s : ℕ) (f : EulerSobolev.Domain 3 → EulerSobolev.Domain q) (hf : ContDiff ℝ (↑⊤) f) : tensorSobolevNorm s (⇑(EulerSobolev.complexify q) ∘ f) = realTensorSobolevNorm q s f

theorem EulerSmoothSobolev.real_smooth_fderiv_le_H3 (q : ℕ) (f : EulerSobolev.Domain 3 → EulerSobolev.Domain q) (hf : ContDiff ℝ (↑⊤) f) (hfL2 : ∀ j ≤ 3, MeasureTheory.MemLp (iteratedFDeriv ℝ j f) 2 MeasureTheory.volume) (x : EulerSobolev.Domain 3) : ‖fderiv ℝ f x‖ ≤ 9 * smoothEmbeddingConstant * realTensorSobolevNorm q 3 f

Real vector-valued H³ to C¹ on R³, for general smooth functions with actual L² derivatives.