Translating the normalized Gaussian field in time

The positive initial time in lem:bu-gaussian is obtained by translating the already rescaled field by one sixth of a unit.

def ESS.buGaussianTimeShiftHomeomorph (σ : ℝ) : CKN.Foundation.Parabolic.Vec3 × ℝ ≃ₜ CKN.Foundation.Parabolic.Vec3 × ℝ

Translation by σ in the time coordinate, leaving the spatial coordinate unchanged.

Equations

• ESS.buGaussianTimeShiftHomeomorph σ = (Homeomorph.refl CKN.Foundation.Parabolic.Vec3).prodCongr (Homeomorph.addLeft σ)

noncomputable def ESS.buGaussianTimeShiftPoint (σ : ℝ) : CKN.Foundation.Parabolic.ParabolicPoint ≃ₜ CKN.Foundation.Parabolic.ParabolicPoint

The parabolic homeomorphism translating time forward by σ. (lem:bu-gaussian#time-shift).

Equations

• ESS.buGaussianTimeShiftPoint σ = CKN.Foundation.Parabolic.parabolicHomeomorph.trans ((ESS.buGaussianTimeShiftHomeomorph σ).trans CKN.Foundation.Parabolic.parabolicHomeomorph.symm)

theorem ESS.buGaussian_timeShift_point_symm_apply (σ : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : (buGaussianTimeShiftPoint σ).symm z = (z.1, z.2 - σ)

Evaluation of the inverse time translation in normalized coordinates.

theorem ESS.buGaussian_timeShift_inverse (σ : ℝ) : (buGaussianTimeShiftPoint σ).symm = buGaussianTimeShiftPoint (-σ)

Inverting the time translation is the translation by the negative amount.

theorem ESS.buGaussian_timeShift_measurePreserving (σ : ℝ) : MeasureTheory.MeasurePreserving (⇑(buGaussianTimeShiftPoint σ)) MeasureTheory.volume MeasureTheory.volume

Time translation preserves parabolic volume (lem:bu-gaussian#time-shift).

theorem ESS.buGaussian_timeShift_image (ρ σ : ℝ) : ⇑(buGaussianTimeShiftPoint σ) '' CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo 0 (2 - σ)) = CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo σ 2)

Time translation maps the source interval onto its positive-time image (lem:bu-gaussian#time-shift).

theorem ESS.buGaussian_timeShift_test_derivatives (σ : ℝ) {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (j : Fin 3) : CKN.spatialPartial (ψ ∘ ⇑(buGaussianTimeShiftHomeomorph σ)) j z = CKN.spatialPartial ψ j ((buGaussianTimeShiftPoint σ) z) ∧ CKN.timePartial (ψ ∘ ⇑(buGaussianTimeShiftHomeomorph σ)) z = CKN.timePartial ψ ((buGaussianTimeShiftPoint σ) z)

Spatial and time derivatives commute with parabolic time translation.

theorem ESS.buGaussian_timeShift_weak_derivatives {ρ σ : ℝ} {w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hweak : CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo 0 (2 - σ)) w Dw D2w Dtw) : CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo σ 2) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => w ((buGaussianTimeShiftPoint σ).symm z)) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => Dw ((buGaussianTimeShiftPoint σ).symm z) i j) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j k : Fin 3) => D2w ((buGaussianTimeShiftPoint σ).symm z) i j k) fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => Dtw ((buGaussianTimeShiftPoint σ).symm z) i

Time translation transports all three weak integration-by-parts identities from a short interval onto its positive-time image.

theorem ESS.buGaussian_timeShift_ae {ρ σ : ℝ} {P : CKN.Foundation.Parabolic.ParabolicPoint → Prop} (hP : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo 0 (2 - σ))), P z) : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo σ 2)), P ((buGaussianTimeShiftPoint σ).symm z)

Almost-everywhere statements on a cylinder commute with the positive-time translation.