The time derivative of a strong solution is bounded in L² on positive-time slices #
prop:lps-smoothing: a uniform L² bound on the time-difference quotients transfers to the weak
time derivative for almost every time, since the pairings of the quotients converge to the pairing
of the derivative at almost every time.
theorem
ESS.lps_ae_slice_memLp_of_slab
{a b : ℝ}
{F : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioo a b)))
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, t)) 2 MeasureTheory.volume
Slices of a square-integrable slab field are square integrable for almost every time.
theorem
ESS.lps_dtu_slice_bound_of_difference_bound
{t₀ T t₁ B h₀ : ℝ}
(hT : t₀ < T)
(ht₁ : t₀ ≤ 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))
(hB : 0 ≤ B)
(hh₀ : 0 < h₀)
(hbound :
∀ h ∈ Set.Ioo 0 h₀,
∀ t ∈ Set.Icc t₁ (T - h),
∀ (i : Fin 3), ∫ (x : CKN.Foundation.Parabolic.Vec3), (1 / h * (u (x, t + h) i - u (x, t) i)) ^ 2 ≤ B)
:
A uniform L² bound on the time-difference quotients of a strong solution on [t₁, T - h]
for all small h bounds the weak time derivative in L² at almost every time of (t₁, T)
(prop:lps-smoothing).