Almost everywhere data on affine time intervals

The heat inequality pulls back from the physical initial interval to the shifted interval in lem:bu-small-time.

theorem ESS.bu_affine_ae_pullback_interval (τ scale a b : ℝ) (hscale : 0 < scale) (P : CKN.Foundation.Parabolic.ParabolicPoint → Prop) (hP : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b))), P z) : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo a b)), P (buAffinePoint τ scale z)

Almost everywhere statements pull back along a positive affine parabolic change of variables between corresponding time intervals.