Assembly support for the local strong solution #
The datum in prop:lps-local-strong is given as a good time of its constant
extension. These lemmas transfer that hypothesis to the zero-based
regularized construction and record the finite squared H¹ energy of the
datum.
theorem
ESS.LPS.lps_constant_initial_good_time_at_zero
{t₀ : ℝ}
(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) t₀)
:
IsLpsGoodTime (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => b z.1)
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => Db z.1 i) 0
A constant-in-time good datum is also a good datum at time zero
(prop:lps-local-strong).
theorem
ESS.lps_local_strong :
∃ (c : ℝ),
0 < c ∧ ∀ (t₀ : ℝ) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3)
(Db : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3),
IsLpsGoodTime (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => b z.1)
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => Db z.1 i) t₀ →
∃ (τ : ℝ),
0 < τ ∧ 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) ≤ τ ∧ ∃ (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du :
CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (p :
CKN.Foundation.Parabolic.ParabolicPoint → ℝ),
IsLpsStrongSolution t₀ (t₀ + τ) u Du p ∧ (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t₀)) =ᵐ[MeasureTheory.volume] b ∧ Filter.Tendsto
(fun (s : ℝ) =>
MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, s) - b x) 2
MeasureTheory.volume)
(nhdsWithin t₀ (Set.Ioi t₀)) (nhds 0) ∧ (∀ (s t : ℝ),
s ∈ Set.Icc t₀ (t₀ + τ) →
t ∈ Set.Icc t₀ (t₀ + τ) →
s ≤ t →
(∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i ^ 2) + 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo s t), ∑ i : Fin 3, ∑ j : Fin 3, Du z i j ^ 2 = ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, s) i ^ 2) ∧ CKN.IsLerayHopfSolution τ b
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => u (z.1, t₀ + z.2))
fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => Du (z.1, t₀ + z.2) i
prop:lps-local-strong: for every solenoidal H¹ datum there is a strong solution on [t₀, t₀ + τ]
with τ ≥ c (1 + ‖b‖_{H¹})⁻⁴ for an absolute constant c, with its initial trace, the energy
equality between any two times, and the Leray--Hopf property. The solution is the limit of the
regularized solutions of lem:lps-regularized-Hk-start, translated in time.