Regularized initial data in ordered Sobolev spaces

The physical regularization kernel contracts the integer Sobolev norm of weak initial data, uniformly in its scale (eq:lps-Hm-energy).

theorem ESS.lps_regUniformMollifiedInitial_smooth (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (ha : CKN.IsInJ a) (i : Fin 3) : ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regUniformMollifiedInitial ρ ε hε a x i

The actual mollified initial state is smooth in space even when its input is only in J (thm:regularised of the CKN manuscript).

theorem ESS.lps_regUniformMollifiedInitial_weak_sobolevNormSq_le (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (ha : CKN.IsInJ a) {m : ℕ} {D : Fin 3 → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ} (hD : ∀ (i : Fin 3), CKN.IsSobolevFamilyOn m Set.univ (fun (x : CKN.Foundation.Parabolic.Vec3) => a x i) (D i)) : (∑ i : Fin 3, CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regUniformMollifiedInitial ρ ε hε a x i) ≤ ∑ i : Fin 3, CKN.sobolevNormSqOn m Set.univ (D i)

The regularized initial state has no larger ordered H^m energy than its specified weak Sobolev derivative family (eq:lps-Hm-energy).