Measurability of the slice L∞ norm #
For a jointly measurable velocity, the essential supremum of the Euclidean norm
of its time slices is a measurable function of time. This is used to integrate
the endpoint Serrin coefficient in lem:lps-comparison.
theorem
ESS.lps_aesm_slab_to_prod
{a b : ℝ}
{E : Type}
[TopologicalSpace E]
{F : CKN.Foundation.Parabolic.ParabolicPoint → E}
(hF : MeasureTheory.AEStronglyMeasurable F (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b))))
:
MeasureTheory.AEStronglyMeasurable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => F z)
(MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo a b)))
Almost everywhere strong measurability on a slab gives measurability on the product space with the product slab measure.
theorem
ESS.lps_essSup_norm_slice_aemeasurable
{a b : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b))))
:
AEMeasurable
(fun (t : ℝ) =>
essSup
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))))
MeasureTheory.volume)
(MeasureTheory.volume.restrict (Set.Ioo a b))
The essential supremum of the Euclidean norm of the time slices of a space-time velocity is an almost everywhere measurable function of time.
theorem
ESS.lps_endpoint_norm_slice_facts
{a b : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b))))
(hEndpoint :
∫⁻ (t : ℝ) in Set.Ioo a b, essSup
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))))
MeasureTheory.volume ^ 2 < ⊤)
:
AEMeasurable
(fun (τ : ℝ) =>
ENNReal.ofReal
(MeasureTheory.eLpNorm
(fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, τ))) ⊤
MeasureTheory.volume).toReal)
(MeasureTheory.volume.restrict (Set.Ioo a b)) ∧ ∫⁻ (τ : ℝ) in Set.Ioo a b, ENNReal.ofReal
(MeasureTheory.eLpNorm
(fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, τ))) ⊤
MeasureTheory.volume).toReal ^ 2 < ⊤ ∧ (∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, τ)) ≤ (MeasureTheory.eLpNorm
(fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, τ))) ⊤
MeasureTheory.volume).toReal) ∧ MeasureTheory.IntegrableOn
(fun (τ : ℝ) =>
(MeasureTheory.eLpNorm
(fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, τ))) ⊤
MeasureTheory.volume).toReal ^ 2)
(Set.Ioo a b) MeasureTheory.volume
The endpoint Serrin coefficient: the L∞ norm of the slices, its
measurability, its square moment, and its pointwise bound on the Euclidean
norm of the velocity.