Joint measurability of mollified pairings

The mollified components and their tested fluxes are almost everywhere strongly measurable jointly in time and the mollification point. They are the integrands exchanged in the cross-testing identity of lem:pv-serrin-uniqueness.

theorem ESS.serrin_quasiMeasurePreserving_triple (T : ℝ) : MeasureTheory.QuasiMeasurePreserving (fun (w : (ℝ × CKN.Foundation.Parabolic.Vec3) × CKN.Foundation.Parabolic.Vec3) => (w.2, w.1.1)) (((MeasureTheory.volume.restrict (Set.Ioo 0 T)).prod MeasureTheory.volume).prod MeasureTheory.volume) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))

Reading a space-time field at (x, τ) from the triple ((τ, y), x) preserves null sets.

theorem ESS.serrin_aesm_prod {E : Type} [TopologicalSpace E] {T : ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → E} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) : MeasureTheory.AEStronglyMeasurable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))

Almost everywhere strong measurability on the parabolic slab, in product coordinates.

theorem ESS.serrin_aesm_triple {E : Type} [TopologicalSpace E] {T : ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → E} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) : MeasureTheory.AEStronglyMeasurable (fun (w : (ℝ × CKN.Foundation.Parabolic.Vec3) × CKN.Foundation.Parabolic.Vec3) => f (w.2, w.1.1)) (((MeasureTheory.volume.restrict (Set.Ioo 0 T)).prod MeasureTheory.volume).prod MeasureTheory.volume)

A space-time field read at (x, τ) from the triple ((τ, y), x).

theorem ESS.serrinMol_aestronglyMeasurable {T : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) {ρ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hρ : Continuous ρ) (k : Fin 3) : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × CKN.Foundation.Parabolic.Vec3) => serrinMol u ρ k z.2 z.1) ((MeasureTheory.volume.restrict (Set.Ioo 0 T)).prod MeasureTheory.volume)

The mollified component is jointly almost everywhere strongly measurable.

theorem ESS.serrinMolFlux_aestronglyMeasurable {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 → ℝ} (hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hDu : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hp : MeasureTheory.AEStronglyMeasurable p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) {ρ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hρ : ContDiff ℝ (↑⊤) ρ) (k : Fin 3) : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × CKN.Foundation.Parabolic.Vec3) => serrinMolFlux u Du p ρ k z.2 z.1) ((MeasureTheory.volume.restrict (Set.Ioo 0 T)).prod MeasureTheory.volume)

The tested flux of the mollified component is jointly almost everywhere strongly measurable.