The base of the regularity ladder #
prop:lps-smoothing: a strong solution has an L²(I; H³) family with L²-continuous H²
slices on [t₀ + δ, T] for every δ > 0. Almost every slice has a uniformly bounded H²
energy (the H² bound of the slice equation together with the uniform bound of the time
derivative), so the convection field is an L²(I; H¹) family and the heat gain applies.
theorem
ESS.lps_sliceH2_ae_bound
{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}
(hsol : IsLpsStrongSolution t₀ T u Du p)
(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))))
{δ : ℝ}
(hδ : 0 < δ)
(hδT : t₀ + δ < T)
:
The H² energy of the slices of a strong solution is uniformly bounded for almost every
time in (t₀ + δ/2, T) (prop:lps-smoothing).