Sobolev contraction of normalized convolution

For a smooth compactly supported kernel of mass one, ordered spatial derivatives commute with convolution, and each differentiated component contracts in L². This supplies the scale-independent mollifier step in eq:lps-Hm-energy.

theorem ESS.lps_wordDeriv_convolution {κ f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hκ : ContDiff ℝ (↑⊤) κ) (hκc : HasCompactSupport κ) (hf : ContDiff ℝ (↑⊤) f) (hfL2 : ∀ (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α f) 2 MeasureTheory.volume) (α : List (Fin 3)) : CKN.wordDeriv α (MeasureTheory.convolution κ f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) = MeasureTheory.convolution κ (CKN.wordDeriv α f) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

Ordered derivatives of a smooth L² field commute with a compact smooth scalar convolution (eq:lps-Hm-energy).

theorem ESS.lps_wordDeriv_convolution_eLpNorm_le {κ f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hκ : ContDiff ℝ (↑⊤) κ) (hκc : HasCompactSupport κ) (hκnonneg : ∀ (x : CKN.Foundation.Parabolic.Vec3), 0 ≤ κ x) (hκone : ∫ (x : CKN.Foundation.Parabolic.Vec3), κ x = 1) (hf : ContDiff ℝ (↑⊤) f) (hfL2 : ∀ (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α f) 2 MeasureTheory.volume) (α : List (Fin 3)) : MeasureTheory.eLpNorm (CKN.wordDeriv α (MeasureTheory.convolution κ f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume)) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm (CKN.wordDeriv α f) 2 MeasureTheory.volume

Normalized nonnegative convolution contracts every ordered spatial derivative in L² (eq:lps-Hm-energy).

theorem ESS.lps_wordDeriv_convolution_memLp {κ f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hκ : ContDiff ℝ (↑⊤) κ) (hκc : HasCompactSupport κ) (hκnonneg : ∀ (x : CKN.Foundation.Parabolic.Vec3), 0 ≤ κ x) (hκone : ∫ (x : CKN.Foundation.Parabolic.Vec3), κ x = 1) (hf : ContDiff ℝ (↑⊤) f) (hfL2 : ∀ (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α f) 2 MeasureTheory.volume) (α : List (Fin 3)) : MeasureTheory.MemLp (CKN.wordDeriv α (MeasureTheory.convolution κ f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume)) 2 MeasureTheory.volume

Every ordered derivative of a normalized convolution stays in L² (eq:lps-Hm-energy).

theorem ESS.lps_integral_sq_le_of_eLpNorm_le {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) (hfg : MeasureTheory.eLpNorm f 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm g 2 MeasureTheory.volume) : ∫ (x : CKN.Foundation.Parabolic.Vec3), f x ^ 2 ≤ ∫ (x : CKN.Foundation.Parabolic.Vec3), g x ^ 2

An L² seminorm comparison between real fields compares their quadratic energy integrals (eq:lps-Hm-energy).

theorem ESS.lps_sobolevNormSq_convolution_le {κ f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hκ : ContDiff ℝ (↑⊤) κ) (hκc : HasCompactSupport κ) (hκnonneg : ∀ (x : CKN.Foundation.Parabolic.Vec3), 0 ≤ κ x) (hκone : ∫ (x : CKN.Foundation.Parabolic.Vec3), κ x = 1) (hf : ContDiff ℝ (↑⊤) f) (hfL2 : ∀ (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α f) 2 MeasureTheory.volume) (m : ℕ) : (CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α (MeasureTheory.convolution κ f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume)) ≤ CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α f

The full ordered integer H^m energy contracts under normalized nonnegative convolution, with constant one at every order (eq:lps-Hm-energy).