Almost every time slice of a strong solution #
For a strong solution with space-time weak derivatives, almost every time slice
has square-integrable velocity, first and second derivatives and time
derivative, the weak-gradient relations between them, and vanishing gradient
trace (lem:lps-H1-estimate).
theorem
ESS.lps_slice_memLp_two_ae_slab
{a b : ℝ}
{E : Type}
[NormedAddCommGroup E]
{F : CKN.Foundation.Parabolic.ParabolicPoint → E}
(hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet 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
Almost every time slice of a square-integrable space-time field on a slab is square integrable.
theorem
ESS.lps_strong_good_slices
{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}
(hU : IsLpsStrongSolution t₀ t₁ u Du p)
(hD : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ t₁) u Du D2u Dtu)
(hMu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))))
(hMDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))))
(hMD2 : MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))))
(hMDt : MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))))
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo t₀ t₁), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => Dtu (x, t)) 2 MeasureTheory.volume ∧ MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => D2u (x, t)) 2 MeasureTheory.volume ∧ (∀ (i j : Fin 3),
CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Foundation.Parabolic.Vec3) => Du (x, t) i j)
fun (x : CKN.Vec 3) (k : Fin 3) => D2u (x, t) i j k) ∧ ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, Du (x, t) i i = 0
The good slices of a strong solution with space-time weak derivatives: the
time derivative and the second derivatives are square integrable, the second
derivatives are the weak gradients of the first derivatives, and the gradient
trace vanishes (lem:lps-H1-estimate).