Smooth tests in affine parabolic coordinates

The pullback of a compactly supported smooth test remains an admissible test on the image time slab in lem:bu-iterate.

noncomputable def ESS.buAffineHomeomorph (τ scale : ℝ) (hscale : 0 < scale) : CKN.Foundation.Parabolic.Vec3 × ℝ ≃ₜ CKN.Foundation.Parabolic.Vec3 × ℝ

The affine coordinate map as a homeomorphism of the ordinary product space.

Equations

• ESS.buAffineHomeomorph τ scale hscale = (Homeomorph.smulOfNeZero scale ⋯).prodCongr ((Homeomorph.smulOfNeZero (scale ^ 2) ⋯).trans (Homeomorph.addLeft τ))

theorem ESS.buAffineHomeomorph_eq (τ scale : ℝ) (hscale : 0 < scale) : ⇑(buAffineHomeomorph τ scale hscale) = buAffinePoint τ scale

The affine homeomorphism evaluates to the parabolic coordinate map.

theorem ESS.buAffineHomeomorph_symm_eq (τ scale : ℝ) (hscale : 0 < scale) : ⇑(buAffineHomeomorph τ scale hscale).symm = fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => (scale⁻¹ • z.1, (scale ^ 2)⁻¹ * (z.2 - τ))

The inverse affine map has the expected coordinate formula.

theorem ESS.buAffineHomeomorph_symm_contDiff (τ scale : ℝ) (hscale : 0 < scale) : ContDiff ℝ ↑⊤ ⇑(buAffineHomeomorph τ scale hscale).symm

The inverse affine map is smooth on the ordinary product space.

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

The affine image of the unit half-space cylinder is the corresponding time slab.

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

Pulling back a smooth compactly supported test by the inverse affine map gives an admissible test on the image slab.

theorem ESS.bu_affine_integral_comp (τ scale : ℝ) (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))))) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1), 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)), F z

Integration on the normalized half-space cylinder transforms by the parabolic Jacobian of the affine map.