Almost everywhere equality on a slab and on its time slices #
Almost everywhere equality of two fields on a slab gives almost everywhere equality of almost every
time slice, and conversely for almost everywhere measurable fields (prop:lps-local-strong).
theorem
ESS.LPS.lps_slab_slice_ae_eq
{E : Type u_1}
{a b : ℝ}
{f g : CKN.Foundation.Parabolic.Vec3 × ℝ → E}
(h : f =ᵐ[MeasureTheory.volume.restrict (CKN.vlSlab a b)] g)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, s)) =ᵐ[MeasureTheory.volume]
fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, s)
Almost everywhere equality on a slab gives almost everywhere equality of almost every time slice.
theorem
ESS.LPS.lps_slab_ae_eq_of_slices
{E : Type u_1}
[NormedAddCommGroup E]
[SecondCountableTopology E]
[MeasurableSpace E]
[BorelSpace E]
{a b : ℝ}
{f g : CKN.Foundation.Parabolic.Vec3 × ℝ → E}
(hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (CKN.vlSlab a b)))
(hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.volume.restrict (CKN.vlSlab a b)))
(h :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, s)) =ᵐ[MeasureTheory.volume]
fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, s))
:
f =ᵐ[MeasureTheory.volume.restrict (CKN.vlSlab a b)] g
Two almost everywhere measurable fields on a slab whose almost every time slices agree almost everywhere agree almost everywhere on the slab.