Affine coordinates on an arbitrary time interval

The shifted time interval in lem:bu-small-time is transported to the initial interval by a positive parabolic dilation with a time translation.

theorem ESS.buAffinePoint_preimage_interval (τ scale a b : ℝ) (hscale : 0 < scale) : buAffinePoint τ scale ⁻¹' CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b)) = CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo a b)

The affine preimage of a half-space time slab has the expected endpoints.

theorem ESS.buAffineHomeomorph_image_interval (τ scale a b : ℝ) (hscale : 0 < scale) : ⇑(buAffineHomeomorph τ scale hscale) '' CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo a b) = CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b))

The affine image of a half-space time interval is its translated, parabolically dilated interval.

theorem ESS.bu_affine_pullback_test_interval (τ scale a b : ℝ) (hscale : 0 < scale) {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ψ ∈ CKN.spaceTimeTestFunction {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo a b)) : ψ ∘ ⇑(buAffineHomeomorph τ scale hscale).symm ∈ CKN.spaceTimeTestFunction {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b))

Smooth compactly supported tests pull back from the normalized half-space interval to the source time slab.

theorem ESS.bu_affine_integral_comp_interval (τ scale a b : ℝ) (hscale : 0 < scale) (F : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hFm : MeasureTheory.AEStronglyMeasurable F (MeasureTheory.volume.restrict (CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b))))) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo a b), F (buAffinePoint τ scale z) = scale⁻¹ ^ 5 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b)), F z

Integration over any normalized half-space interval transforms by the parabolic Jacobian of the affine map.

theorem ESS.bu_affine_locallyIntegrableOn_interval {E : Type u_1} [NormedAddCommGroup E] (τ scale a b : ℝ) (hscale : 0 < scale) (f : CKN.Foundation.Parabolic.ParabolicPoint → E) (hf : MeasureTheory.LocallyIntegrableOn f (CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b))) MeasureTheory.volume) : MeasureTheory.LocallyIntegrableOn (f ∘ buAffinePoint τ scale) (CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo a b)) MeasureTheory.volume

Local integrability transfers through affine coordinates between any two corresponding positive half-space time intervals.