Uniform H¹ and H² bounds for the regularized solutions

The squared gradient norm y = ‖∇U_ε‖₂² of the regularized velocity satisfies y' + ‖∇²U_ε‖₂² ≤ C y³ with an absolute constant, on every positive time, by the differentiated energy identity and the transport estimate. With the L² energy identity, the scalar comparison of RegularisedH1Comparison gives a common lifespan ≥ c (1 + ‖b‖_{H¹})⁻⁴ and bounds on sup_t ‖U_ε(t)‖_{H¹} and ‖∇²U_ε‖_{L²_{t,x}} independent of ε (prop:lps-local-strong, eq:lps-uniform-H1).

theorem ESS.LPS.lps_norm_sq_eq_integral_of_ae {F : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)} {f : CKN.Foundation.Parabolic.Vec3 → ℝ} (h : ↑↑F =ᵐ[MeasureTheory.volume] f) : ‖F‖ ^ 2 = ∫ (x : CKN.Foundation.Parabolic.Vec3), f x ^ 2

The squared norm of an L² class is the integral of squares of any representative.

theorem ESS.LPS.lps_regR12_word_sq_continuous (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) (i : Fin 3) (α : List (Fin 3)) : Continuous fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv α (fun (y : CKN.Foundation.Parabolic.Vec3) => lpsRegU ρ ε hε b hb (y, max t 0) i) x ^ 2

The squared L² norm of every ordered derivative of the regularized velocity is continuous in time on [0, ∞).

theorem ESS.LPS.lps_eLpNorm_field_sq {f : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.eLpNorm (CKN.Leray.regUniformSpatialField f) 2 MeasureTheory.volume ^ 2 = ENNReal.ofReal (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, f x i ^ 2)

The squared L² seminorm of the Euclidean carrier field of a vector field is the integral of the sum of squared components.

theorem ESS.LPS.lps_regR12_kinetic_le (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {t : ℝ} (ht : 0 ≤ t) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, lpsRegU ρ ε hε b hb (x, t) i ^ 2 ≤ ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, b x i ^ 2

The kinetic energy of the regularized velocity does not exceed that of the datum, by the energy equality (R5) and the contraction of the mollifier.

theorem ESS.LPS.lps_regR12_initial_eq (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) (i : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) : lpsRegU ρ ε hε b hb (x, 0) i = CKN.Leray.regUniformMollifiedInitial ρ ε hε b x i

At time zero the regularized velocity is the mollified datum.

theorem ESS.LPS.lps_regR12_initial_gradient_le (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) (Db : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (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) : lpsRegGradEnergy ρ ε hε b hb 0 ≤ ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Db x i j ^ 2

The initial gradient energy of the regularized velocity is at most the squared L² norm of the datum's weak gradient.

theorem ESS.LPS.lps_regR12_gradEnergy_continuous (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) : Continuous fun (t : ℝ) => lpsRegGradEnergy ρ ε hε b hb (max t 0)

The gradient energy of the regularized velocity, extended by its time-zero value to negative times, is continuous.

theorem ESS.LPS.lps_regR12_hessEnergy_continuous (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) : Continuous fun (t : ℝ) => lpsRegHessEnergy ρ ε hε b hb (max t 0)

The second-derivative energy of the regularized velocity, extended by its time-zero value to negative times, is continuous.

theorem ESS.LPS.lps_regR12_gradEnergy_nonneg (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) (t : ℝ) : 0 ≤ lpsRegGradEnergy ρ ε hε b hb t

The gradient energy is nonnegative.

theorem ESS.LPS.lps_regR12_hessEnergy_nonneg (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) (t : ℝ) : 0 ≤ lpsRegHessEnergy ρ ε hε b hb t

The second-derivative energy is nonnegative.

theorem ESS.LPS.lps_regR12_gradEnergy_hasDerivAt (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {t : ℝ} (ht : 0 < t) : HasDerivAt (fun (s : ℝ) => lpsRegGradEnergy ρ ε hε b hb (max s 0)) (-2 * lpsRegHessEnergy ρ ε hε b hb t + 2 * lpsRegTransportPairing ρ ε hε b hb t) t

The gradient energy of the regularized velocity has the stated derivative at every positive time (eq:lps-uniform-H1).

theorem ESS.LPS.lps_regR12_cubic_inequality (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {t : ℝ} (ht : 0 < t) : -2 * lpsRegHessEnergy ρ ε hε b hb t + 2 * lpsRegTransportPairing ρ ε hε b hb t + lpsRegHessEnergy ρ ε hε b hb t ≤ 4 * (9 * CKN.gagliardoNirenbergSobolevConstant.toReal ^ (3 / 2)) ^ 4 * lpsRegGradEnergy ρ ε hε b hb t ^ 3

The cubic differential inequality y' + ‖∇²U_ε‖₂² ≤ C y³ for the gradient energy of the regularized velocity, with an absolute constant (eq:lps-uniform-H1).

theorem ESS.LPS.lps_slab_integral_eq_time_integral {f : CKN.Foundation.Parabolic.Vec3 → ℝ → ℝ} {T : ℝ} (hT : 0 ≤ T) (hf : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z.1 z.2) 2 (MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioo 0 T))) : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ Set.Ioo 0 T, f z.1 z.2 ^ 2 = ∫ (t : ℝ) in 0..T, ∫ (x : CKN.Foundation.Parabolic.Vec3), f x t ^ 2

Tonelli identity for a square-integrable function on a slab, in terms of the slice integrals.

theorem ESS.LPS.lps_regR12_hess_slab (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {T : ℝ} (hT : 0 < T) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), ∑ i : Fin 3, ∑ j : Fin 3, (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (k : Fin 3) => CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (fun (v : CKN.Foundation.Parabolic.ParabolicPoint) => lpsRegU ρ ε hε b hb v i) j w) k z) ^ 2 = ∫ (t : ℝ) in 0..T, lpsRegHessEnergy ρ ε hε b hb (max t 0)

The slab integral of the second derivatives of the regularized velocity is the time integral of their slice energies.

theorem ESS.LPS.lps_regR12_gradSq (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {t : ℝ} (ht : 0 ≤ t) : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.spatialGradientSq (lpsRegU ρ ε hε b hb) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => lpsRegU ρ ε hε b hb w i) j z) (x, t)) MeasureTheory.volume ∧ ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialGradientSq (lpsRegU ρ ε hε b hb) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => lpsRegU ρ ε hε b hb w i) j z) (x, t) = lpsRegGradEnergy ρ ε hε b hb t

The gradient integrand of the regularized velocity is integrable on every nonnegative-time slice, with integral the gradient energy.

theorem ESS.LPS.lps_regR12_kineticSq (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {t : ℝ} (ht : 0 ≤ t) : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (lpsRegU ρ ε hε b hb (x, t)) ^ 2) MeasureTheory.volume ∧ ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (lpsRegU ρ ε hε b hb (x, t)) ^ 2 = ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, lpsRegU ρ ε hε b hb (x, t) i ^ 2

The squared velocity of the regularized solution is integrable on every nonnegative-time slice.

theorem ESS.LPS.lps_regularised_uniform_h1_bounds : ∃ (c : ℝ), 0 < c ∧ ∀ (ρ : CKN.Leray.RegMollifierProfile) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (Db : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (hb : IsLpsGoodTime (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => b z.1) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => Db z.1 i) 0), ∃ (T : ℝ) (M : ℝ), 0 < T ∧ c * (1 + √(∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, b x i ^ 2 + ∑ i : Fin 3, ∑ j : Fin 3, Db x i j ^ 2)).rpow (-4) ≤ T ∧ 0 ≤ M ∧ ∀ (ε : ℝ) (hε : 0 < ε), have Uε := CKN.Leray.regR12Velocity ρ ε hε b ⋯; have Dε := fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Uε y i) j z; have D2ε := fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j k : Fin 3) => CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => Uε x i) j y) k z; (∀ t ∈ Set.Icc 0 T, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (Uε (x, t)) ^ 2 + CKN.spatialGradientSq Uε Dε (x, t) ≤ M) ∧ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), ∑ i : Fin 3, ∑ j : Fin 3, CKN.Foundation.Parabolic.vec3EuclideanNorm (D2ε z i j) ^ 2 ≤ M

Uniform H¹/H² bounds for the regularized solutions (prop:lps-local-strong).