Almost-everywhere statements in product coordinates

The canonical space-time homeomorphism preserves the product Lebesgue measure on a normalized cylinder.

theorem ESS.uc_integrableOn_parabolic_to_product (ρ : ℝ) {F : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hF : MeasureTheory.IntegrableOn F (ucCylinder ρ) MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => F (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z)) (CKN.Foundation.Parabolic.vec3Ball 0 ρ ×ˢ Set.Ioo 0 2) MeasureTheory.volume

Integrability on a normalized CKN cylinder transfers to product coordinates through the canonical homeomorphism.