The initial layer of the time-difference quotients #
prop:lps-smoothing: the mean over [t₀, t₀ + δ] of the squared L² norms of the time-difference
quotients of a strong solution is at most the L² norm squared of its weak time derivative.
theorem
ESS.lps_dtu_normSq_integrable
{t₀ T : ℝ}
{Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hDt : MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))))
:
MeasureTheory.Integrable (fun (σ : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, Dtu (x, σ) i ^ 2)
(MeasureTheory.volume.restrict (Set.Ioo t₀ T))
The squared L² norm of the weak time derivative is integrable in time.
theorem
ESS.lps_initial_layer_bound
{t₀ T δ h : ℝ}
(hT : t₀ < T)
(hδ : 0 < δ)
(hh : 0 < h)
(hδhT : t₀ + δ + h ≤ T)
{u Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))))
(hDt : MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))))
(htime :
∀ (i : Fin 3),
∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo t₀ T),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T), u z i * CKN.timePartial φ z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T), Dtu z i * φ z)
(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))
(hEint :
IntervalIntegrable
(fun (τ : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, (1 / h * (u (x, τ + h) i - u (x, τ) i)) ^ 2)
MeasureTheory.volume t₀ (t₀ + δ))
:
The mean over the initial layer [t₀, t₀ + δ] of the squared L² norms of the time-difference
quotients is at most the total L² energy of the weak time derivative (prop:lps-smoothing).