Scale-independent Sobolev contraction

The physical kernel of the regularized equation contracts the ordered integer Sobolev energy of each velocity component. The estimate has constant one and is independent of the mollifier scale.

theorem ESS.lps_regKernel_sobolevNormSq_le (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {f : CKN.Foundation.Parabolic.Vec3 → ℝ} (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 (CKN.Leray.regUniformMollifierKernel ρ ε hε) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume)) ≤ CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α f

The regularization kernel contracts the scalar ordered H^m energy (eq:lps-Hm-energy).

theorem ESS.lps_regKernel_vector_sobolevNormSq_le (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hu : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) (huL2 : ∀ (i : Fin 3) (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) 2 MeasureTheory.volume) (m : ℕ) : (∑ i : Fin 3, CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α (MeasureTheory.convolution (CKN.Leray.regUniformMollifierKernel ρ ε hε) (fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume)) ≤ ∑ i : Fin 3, CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u x i

The regularization kernel contracts the velocity's summed ordered H^m energy (eq:lps-Hm-energy).

theorem ESS.lps_regUniformMollifiedVelocity_component_convolution (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (t : ℝ) (hu : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (x : CKN.Foundation.Parabolic.Vec3) (i : Fin 3) : CKN.Leray.regUniformMollifiedVelocity ρ ε hε u (x, t) i = MeasureTheory.convolution (CKN.Leray.regUniformMollifierKernel ρ ε hε) (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, t) i) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x

On each time slice, the regularized transport velocity is exactly convolution by the physical scalar kernel (eq:reg-mollifier of the CKN manuscript).

theorem ESS.lps_regUniformMollifiedVelocity_smooth_memLp (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (t : ℝ) (hu : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hsmooth : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) (huL2 : ∀ (i : Fin 3) (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) 2 MeasureTheory.volume) : (∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regUniformMollifiedVelocity ρ ε hε u (x, t) i) ∧ ∀ (i : Fin 3) (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regUniformMollifiedVelocity ρ ε hε u (x, t) i) 2 MeasureTheory.volume

A smooth velocity slice with square-integrable ordered derivatives has a smooth mollified slice with the same L² derivative property (eq:lps-Hm-energy).

theorem ESS.lps_regUniformMollifiedVelocity_sobolevNormSq_le (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (t : ℝ) (hu : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hsmooth : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) (huL2 : ∀ (i : Fin 3) (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) 2 MeasureTheory.volume) (m : ℕ) : (∑ i : Fin 3, CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regUniformMollifiedVelocity ρ ε hε u (x, t) i) ≤ ∑ i : Fin 3, CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i

The actual regularized transport velocity contracts the whole ordered H^m energy on each smooth time slice (eq:lps-Hm-energy).