Scalar chain-rule consequences for the strong H¹ estimate #
An ordered interval identity with an integrable density gives absolute
continuity and the corresponding almost-everywhere derivative
(lem:lps-H1-estimate).
theorem
ESS.LPS.lps_h1_chain_density_integrable
{a b : ℝ}
{Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3}
(hDtu : MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b))))
(hD2u : MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b))))
:
MeasureTheory.MemLp
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, Dtu z i * ∑ j : Fin 3, D2u z i j j) 1
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b))) ∧ MeasureTheory.IntegrableOn
(fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, Dtu (x, t) i * ∑ j : Fin 3, D2u (x, t) i j j)
(Set.Ioo a b) MeasureTheory.volume ∧ MeasureTheory.Integrable
(fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) =>
∑ i : Fin 3,
Dtu (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z) i * ∑ j : Fin 3, D2u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z) i j j)
(MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo a b)))
The scalar contraction of the time derivative with the vector Laplacian
is integrable in time when both spacetime fields are square integrable
(lem:lps-H1-estimate).
theorem
ESS.LPS.lps_h1_chain_setIntegral_eq_intervalIntegral
{a b s t : ℝ}
{q : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hq : MeasureTheory.Integrable q (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo a b))))
(hs : s ∈ Set.Icc a b)
(ht : t ∈ Set.Icc a b)
(hst : s ≤ t)
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo s t), q (CKN.Foundation.Parabolic.parabolicHomeomorph z) = ∫ (r : ℝ) in s..t, ∫ (x : CKN.Foundation.Parabolic.Vec3), q (x, r)
Product Fubini identifies the strong-solution chain density on any
subinterval with the interval integral of its spatial slice integral
(lem:lps-H1-estimate).
theorem
ESS.LPS.lps_ac_of_ordered_interval_integral
{a b : ℝ}
{f g : ℝ → ℝ}
(hab : a ≤ b)
(hg : MeasureTheory.IntegrableOn g (Set.Icc a b) MeasureTheory.volume)
(hfg : ∀ (s t : ℝ), s ∈ Set.Icc a b → t ∈ Set.Icc a b → s ≤ t → f t = f s + ∫ (r : ℝ) in s..t, g r)
:
An ordered-interval integral identity identifies the derivative of the
energy almost everywhere (lem:lps-H1-estimate).
theorem
ESS.LPS.lps_h1_energy_ac_of_ordered_identity
{a b : ℝ}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3}
(hab : a ≤ b)
(hDtu : MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b))))
(hD2u : MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b))))
(hIdentity :
∀ (s t : ℝ),
s ∈ Set.Icc a b →
t ∈ Set.Icc a b →
s ≤ t →
∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Du (x, t) i j ^ 2 = (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Du (x, s) i j ^ 2) - 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo s t), ∑ i : Fin 3, Dtu z i * ∑ j : Fin 3, D2u z i j j)
:
AbsolutelyContinuousOnInterval
(fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Du (x, t) i j ^ 2) a b ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), deriv (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Du (x, t) i j ^ 2) t = -2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, Dtu (x, t) i * ∑ j : Fin 3, D2u (x, t) i j j
The D3c ordered H¹ identity supplies absolute continuity and its
almost-everywhere derivative on the closed interval
(lem:lps-H1-estimate).