Almost-everywhere equality on a slab and on its time slices #
Almost-everywhere equality of two measurable fields on a slab is equivalent to
almost-everywhere equality of almost every pair of time slices
(lem:lps-continuation).
theorem
ESS.lps_ae_slab_to_prod
{a b : ℝ}
{P : CKN.Foundation.Parabolic.ParabolicPoint → Prop}
(h :
∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)), P z)
:
Almost-everywhere statements on a slab transfer to the product slab measure.
theorem
ESS.lps_ae_prod_to_slab
{a b : ℝ}
{P : CKN.Foundation.Parabolic.ParabolicPoint → Prop}
(h :
∀ᵐ (q : CKN.Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo a b)), P (CKN.Foundation.Parabolic.parabolicHomeomorph.symm q))
:
The converse transfer to the product slab measure.
theorem
ESS.lps_ae_slices_of_prod
{a b : ℝ}
{P : CKN.Foundation.Parabolic.Vec3 × ℝ → Prop}
(h :
∀ᵐ (q : CKN.Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo a b)), P q)
:
From almost-everywhere validity on ℝ³ × (a,b) to almost every time slice.
theorem
ESS.lps_ae_prod_of_slices
{a b : ℝ}
{P : CKN.Foundation.Parabolic.Vec3 × ℝ → Prop}
(hP : MeasurableSet {q : CKN.Foundation.Parabolic.Vec3 × ℝ | P q})
(h : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), P (x, t))
:
∀ᵐ (q : CKN.Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo a b)), P q
From almost every time slice to almost-everywhere validity, for a measurable condition.
theorem
ESS.lps_slices_ae_eq_of_slab
{a b : ℝ}
{E : Type}
{F G : CKN.Foundation.Parabolic.ParabolicPoint → E}
(h : F =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b))] G)
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), (fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, t)) =ᵐ[MeasureTheory.volume]
fun (x : CKN.Foundation.Parabolic.Vec3) => G (x, t)
Almost-everywhere equality on a slab gives almost-everywhere equality of almost every pair of time slices.
theorem
ESS.lps_slab_ae_eq_of_slices
{a b : ℝ}
{E : Type}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
{F G : CKN.Foundation.Parabolic.ParabolicPoint → E}
(hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b))))
(hG : MeasureTheory.MemLp G 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b))))
(h :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), (fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, t)) =ᵐ[MeasureTheory.volume]
fun (x : CKN.Foundation.Parabolic.Vec3) => G (x, t))
:
F =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b))] G
Almost-everywhere equality of almost every pair of time slices gives almost-everywhere equality on the slab, for square-integrable fields.