A common comparison interval for regularized H¹ energies

The scalar H¹ differential inequality gives the same lifespan for an entire family of regularizations. The interval below has the fourth-power dependence on the H¹ size used by prop:lps-local-strong.

theorem ESS.LPS.lps_h1_family_common_lifespan_bound {ι : Type} {C E₀ : ℝ} (hC : 0 ≤ C) (hE₀ : 0 ≤ E₀) (y dy d : ι → ℝ → ℝ) (hy : ∀ (k : ι), Continuous (y k)) (hd : ∀ (k : ι), Continuous (d k)) (henergy : ∀ (k : ι), ∀ t ∈ Set.Ioo 0 ((1 + √E₀).rpow (-4) / (8 * (1 + C))), HasDerivAt (y k) (dy k t) t) (hnonneg : ∀ (k : ι), ∀ t ∈ Set.Icc 0 ((1 + √E₀).rpow (-4) / (8 * (1 + C))), 0 ≤ y k t ∧ 0 ≤ d k t) (hineq : ∀ (k : ι), ∀ t ∈ Set.Ioo 0 ((1 + √E₀).rpow (-4) / (8 * (1 + C))), dy k t + d k t ≤ C * y k t ^ 3) (hinit : ∀ (k : ι), y k 0 ≤ E₀) : 0 < (1 + √E₀).rpow (-4) / (8 * (1 + C)) ∧ ∀ (k : ι), ∀ t ∈ Set.Icc 0 ((1 + √E₀).rpow (-4) / (8 * (1 + C))), y k t + ∫ (s : ℝ) in 0..t, d k s ≤ 2 * (1 + E₀)

A family satisfying one cubic H¹ differential inequality has a common lifespan and a uniform energy plus dissipation bound. The interval depends only on the common differential constant and the initial squared H¹ bound (prop:lps-local-strong).

theorem ESS.LPS.lps_h1_family_spatial_uniform_bound {ι : Type} {T E₀ : ℝ} (hT : 0 < T) (hE₀ : 0 ≤ E₀) (K G y d Q : ι → ℝ → ℝ) (hK : ∀ (k : ι), ∀ t ∈ Set.Icc 0 T, K k t ≤ E₀) (hG : ∀ (k : ι), ∀ t ∈ Set.Icc 0 T, G k t ≤ y k t) (hynonneg : ∀ (k : ι), ∀ t ∈ Set.Icc 0 T, 0 ≤ y k t) (hdnonneg : ∀ (k : ι), ∀ t ∈ Set.Icc 0 T, 0 ≤ d k t) (hcompare : ∀ (k : ι), ∀ t ∈ Set.Icc 0 T, y k t + ∫ (s : ℝ) in 0..t, d k s ≤ 2 * (1 + E₀)) (hQ : ∀ (k : ι), Q k T ≤ ∫ (s : ℝ) in 0..T, d k s) (k : ι) : (∀ t ∈ Set.Icc 0 T, K k t + G k t ≤ 3 * (1 + E₀)) ∧ Q k T ≤ 3 * (1 + E₀)

The common scalar comparison controls both the spatial H¹ slices and the integrated second-derivative dissipation once the kinetic energy is bounded by the initial datum (prop:lps-local-strong).

noncomputable def ESS.LPS.lpsH1ComparisonTime (E₀ C : ℝ) : ℝ

The scalar comparison interval determined by initial squared H¹ energy and the cubic differential constant.

Equations

• ESS.LPS.lpsH1ComparisonTime E₀ C = (1 + √E₀).rpow (-4) / (8 * (1 + C))

theorem ESS.LPS.lps_good_datum_h1_energy_integrable (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (Db : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (hGood : IsLpsGoodTime (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => b z.1) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => Db z.1 i) 0) : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ i : Fin 3, b x i ^ 2 + ∑ i : Fin 3, ∑ j : Fin 3, Db x i j ^ 2) MeasureTheory.volume ∧ 0 ≤ ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, b x i ^ 2 + ∑ i : Fin 3, ∑ j : Fin 3, Db x i j ^ 2

The componentwise squared H¹ energy of a good datum is integrable and nonnegative (prop:lps-local-strong).

theorem ESS.LPS.lps_regularised_uniform_h1_bounds_of_energy_estimates (ρ : CKN.Leray.RegMollifierProfile) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (Db : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (hGood : IsLpsGoodTime (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => b z.1) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => Db z.1 i) 0) (C : ℝ) (hC : 0 ≤ C) (y dy d : ℝ → ℝ → ℝ) (hy : ∀ (ε : ℝ), Continuous (y ε)) (hd : ∀ (ε : ℝ), Continuous (d ε)) (henergy : ∀ (ε : ℝ), 0 < ε → ∀ t ∈ Set.Ioo 0 ((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) / (8 * (1 + C))), HasDerivAt (y ε) (dy ε t) t) (hnonneg : ∀ (ε : ℝ), 0 < ε → ∀ t ∈ Set.Icc 0 ((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) / (8 * (1 + C))), 0 ≤ y ε t ∧ 0 ≤ d ε t) (hineq : ∀ (ε : ℝ), 0 < ε → ∀ t ∈ Set.Ioo 0 ((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) / (8 * (1 + C))), dy ε t + d ε t ≤ C * y ε t ^ 3) (hinit : ∀ (ε : ℝ), 0 < ε → y ε 0 ≤ ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, b x i ^ 2 + ∑ i : Fin 3, ∑ j : Fin 3, Db x i j ^ 2) (hkinetic : ∀ (ε : ℝ) (hε : 0 < ε), ∀ t ∈ Set.Icc 0 ((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) / (8 * (1 + C))), ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (CKN.Leray.regR12Velocity ρ ε hε b ⋯ (x, t)) ^ 2 ≤ ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, b x i ^ 2 + ∑ i : Fin 3, ∑ j : Fin 3, Db x i j ^ 2) (hgradient : ∀ (ε : ℝ) (hε : 0 < ε), ∀ t ∈ Set.Icc 0 ((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) / (8 * (1 + C))), ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialGradientSq (CKN.Leray.regR12Velocity ρ ε hε b ⋯) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Leray.regR12Velocity ρ ε hε b ⋯ w i) j z) (x, t) ≤ y ε t) (hkineticIntegrable : ∀ (ε : ℝ) (hε : 0 < ε), ∀ t ∈ Set.Icc 0 ((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) / (8 * (1 + C))), MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (CKN.Leray.regR12Velocity ρ ε hε b ⋯ (x, t)) ^ 2) MeasureTheory.volume) (hgradientIntegrable : ∀ (ε : ℝ) (hε : 0 < ε), ∀ t ∈ Set.Icc 0 ((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) / (8 * (1 + C))), MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.spatialGradientSq (CKN.Leray.regR12Velocity ρ ε hε b ⋯) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Leray.regR12Velocity ρ ε hε b ⋯ w i) j z) (x, t)) MeasureTheory.volume) (hsecond : ∀ (ε : ℝ) (hε : 0 < ε), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 (lpsH1ComparisonTime (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, b x i ^ 2 + ∑ i : Fin 3, ∑ j : Fin 3, Db x i j ^ 2) C)), ∑ 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) => CKN.Leray.regR12Velocity ρ ε hε b ⋯ v i) j w) k z) ^ 2 ≤ intervalIntegral (d ε) 0 (lpsH1ComparisonTime (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, b x i ^ 2 + ∑ i : Fin 3, ∑ j : Fin 3, Db x i j ^ 2) C) MeasureTheory.volume) : ∃ (T : ℝ) (M : ℝ), 0 < T ∧ 1 / (8 * (1 + 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 (w : CKN.Foundation.Parabolic.ParabolicPoint) => Uε w i) j z; have D2ε := fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j k : Fin 3) => CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (fun (v : CKN.Foundation.Parabolic.ParabolicPoint) => Uε v i) j w) 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

The scalar comparison and the regularized kinetic-energy estimate give the exact ε-uniform slice-H¹ and space-time-H² bound used by the compactness argument (prop:lps-local-strong). The assumptions are the PDE-derived energy identities and physical norm identifications for this particular regularized family.