Uniform bound for the time-difference quotients of a strong solution #
prop:lps-smoothing: the Kiselev–Ladyzhenskaya energy argument. The time-difference quotient of a
strong solution solves a linear Stokes-type system whose flux is bounded by ‖u‖_∞ |v|; its energy
obeys a Grönwall inequality with a coefficient integrable in time, uniformly in the step.
theorem
ESS.lps_kl_energy_identity
{t₀ T h : ℝ}
(hh : 0 < h)
(hhT : h < T - t₀)
{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 → ℝ}
{D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hderiv : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ T) u Du D2u Dtu)
(hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))))
(hDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))))
(hD2u : MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))))
(hDtu : MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))))
(hp : MeasureTheory.MemLp p 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))))
(heq :
∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo t₀ T),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T), ∑ i : Fin 3, Dtu z i * φ z i - ∑ i : Fin 3,
∑ j : Fin 3,
u z i * u z j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3,
∑ j : Fin 3,
Du z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - p z * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0)
(hdiv :
∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)), ∑ i : Fin 3, Du z i i = 0)
(hslice :
∀ t ∈ Set.Icc t₀ T, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume)
(hcont :
∀ t ∈ Set.Icc t₀ T,
Filter.Tendsto
(fun (s : ℝ) =>
MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, s) - u (x, t)) 2 MeasureTheory.volume)
(nhdsWithin t (Set.Icc t₀ T)) (nhds 0))
(hH :
∀ (i j : Fin 3),
MeasureTheory.MemLp
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
1 / h * (u (z.1, z.2 + h) i * u (z.1, z.2 + h) j - u z i * u z j))
2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ (T - h)))))
(s t : ℝ)
:
t₀ ≤ s →
s ≤ t →
t ≤ T - h →
(∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, (1 / h * (u (x, t + h) i - u (x, t) i)) ^ 2) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, (1 / h * (u (x, s + h) i - u (x, s) i)) ^ 2 = ∫ (τ : ℝ) in s..t, (-2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, (1 / h * (Du (x, τ + h) i j - Du (x, τ) i j)) ^ 2) + 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3,
∑ j : Fin 3,
1 / h * (u (x, τ + h) i * u (x, τ + h) j - u (x, τ) i * u (x, τ) j) * (1 / h * (Du (x, τ + h) i j - Du (x, τ) i j))
The energy identity for the time-difference quotient of a strong solution
(prop:lps-smoothing), in scalar form.