H¹ energy control for regularized solutions

The scalar comparison below is the lifespan step for the regularized H¹ energy identity. The PDE pairing supplies its cubic differential inequality.

theorem ESS.LPS.lps_h1_cubic_differential_inequality {C E D E' K : ℝ} (hC : 0 ≤ C) (hE : 0 ≤ E) (hD : 0 ≤ D) (hIdentity : E' + 2 * D = 2 * K) (hTransport : K ≤ C * E.rpow (3 / 4) * D.rpow (3 / 4)) : E' + D ≤ 4 * C ^ 4 * E ^ 3

The pressure-free regularized H¹ identity and its scale-independent transport pairing estimate imply the cubic H¹ differential inequality.

theorem ESS.LPS.lps_regularised_initial_velocity_l2_contraction (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : MeasureTheory.MemLp b 2 MeasureTheory.volume) : MeasureTheory.eLpNorm (CKN.Leray.regUniformSpatialField (CKN.Leray.regUniformMollifiedInitial ρ ε hε b)) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm (CKN.Leray.regUniformSpatialField b) 2 MeasureTheory.volume

The initial regularization is an L² contraction on the spatial vector field (lem:reg-mollifier-bounds of the CKN manuscript).

theorem ESS.LPS.lps_regularised_initial_gradient_row_l2_contraction (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (Db : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) (hH1 : ∀ (i : Fin 3), ∃ (h : CKN.H1Function Set.univ), (h.toFun = fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) ∧ h.grad = fun (x : CKN.Foundation.Parabolic.Vec3) (j : Fin 3) => Db x i j) (i : Fin 3) : MeasureTheory.eLpNorm (CKN.Leray.regUniformSpatialField fun (x : CKN.Foundation.Parabolic.Vec3) (j : Fin 3) => CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regUniformMollifiedInitial ρ ε hε b y i) j x) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm (CKN.Leray.regUniformSpatialField fun (x : CKN.Foundation.Parabolic.Vec3) => Db x i) 2 MeasureTheory.volume

Each first-derivative row of the mollified initial state is an L² contraction of the corresponding weak-gradient row (lem:reg-mollifier-bounds of the CKN manuscript).

theorem ESS.LPS.lps_regularised_initial_h1_energy_bound (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (Db : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) (hH1 : ∀ (i : Fin 3), ∃ (h : CKN.H1Function Set.univ), (h.toFun = fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) ∧ h.grad = fun (x : CKN.Foundation.Parabolic.Vec3) (j : Fin 3) => Db x i j) : MeasureTheory.eLpNorm (CKN.Leray.regUniformSpatialField (CKN.Leray.regUniformMollifiedInitial ρ ε hε b)) 2 MeasureTheory.volume ^ 2 + ∑ i : Fin 3, MeasureTheory.eLpNorm (CKN.Leray.regUniformSpatialField fun (x : CKN.Foundation.Parabolic.Vec3) (j : Fin 3) => CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regUniformMollifiedInitial ρ ε hε b y i) j x) 2 MeasureTheory.volume ^ 2 ≤ MeasureTheory.eLpNorm (CKN.Leray.regUniformSpatialField b) 2 MeasureTheory.volume ^ 2 + ∑ i : Fin 3, MeasureTheory.eLpNorm (CKN.Leray.regUniformSpatialField fun (x : CKN.Foundation.Parabolic.Vec3) => Db x i) 2 MeasureTheory.volume ^ 2

The total squared H¹ energy of the mollified initial state is bounded by the datum's squared H¹ energy (prop:lps-local-strong).

theorem ESS.LPS.lps_h1_scalar_uniform_bound {a T C E₀ : ℝ} {y dy d : ℝ → ℝ} (hC : 0 ≤ C) (hE₀ : 0 ≤ E₀) (haT : a ≤ T) (hTsmall : T - a ≤ 1 / (8 * (1 + C) * (1 + E₀) ^ 2)) (hy : Continuous y) (hd : Continuous d) (henergy : ∀ t ∈ Set.Ioo a T, HasDerivAt y (dy t) t) (hnonneg : ∀ t ∈ Set.Icc a T, 0 ≤ y t ∧ 0 ≤ d t) (hineq : ∀ t ∈ Set.Ioo a T, dy t + d t ≤ C * y t ^ 3) (hinit : y a ≤ E₀) (t : ℝ) : t ∈ Set.Icc a T → y t + ∫ (s : ℝ) in a..t, d s ≤ 2 * (1 + E₀)

A cubic H¹ energy inequality gives a uniform energy and dissipation bound on a lifespan proportional to the inverse square of the initial energy (prop:lps-local-strong).