Affine parabolic coordinates for backward uniqueness

The time iteration and finite-slab arguments in lem:bu-iterate and thm:bu use positive spatial dilation and an affine time change.

def ESS.buAffinePoint (τ scale : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.Foundation.Parabolic.ParabolicPoint

The affine parabolic change of variables based at time τ.

Equations

• ESS.buAffinePoint τ scale z = (scale • z.1, τ + scale ^ 2 * z.2)

def ESS.buAffineField (τ scale : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3

A field in affine parabolic coordinates.

Equations

• ESS.buAffineField τ scale w z = w (ESS.buAffinePoint τ scale z)

def ESS.buAffineDw (τ scale : ℝ) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3

The first spatial weak derivative in affine parabolic coordinates.

Equations

• ESS.buAffineDw τ scale Dw z i j = scale * Dw (ESS.buAffinePoint τ scale z) i j

def ESS.buAffineD2w (τ scale : ℝ) (D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3

The second spatial weak derivative in affine parabolic coordinates.

Equations

• ESS.buAffineD2w τ scale D2w z i j k = scale ^ 2 * D2w (ESS.buAffinePoint τ scale z) i j k

def ESS.buAffineDtw (τ scale : ℝ) (Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3

The weak time derivative in affine parabolic coordinates.

Equations

• ESS.buAffineDtw τ scale Dtw z i = scale ^ 2 * Dtw (ESS.buAffinePoint τ scale z) i

theorem ESS.buAffinePoint_eq_scalingParabolic (τ scale : ℝ) : buAffinePoint τ scale = CKN.scalingParabolic scale (0, τ)

The affine coordinates agree with the parabolic dilation and translation used by the integration change-of-variables formulas.

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

The inverse image of a time slab under the affine map is the unit positive-time cylinder.

theorem ESS.buAffinePoint_mem_halfCylinder (τ scale : ℝ) (hτ : 0 ≤ τ) (hscale : 0 < scale) (hupper : τ + scale ^ 2 ≤ 1) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1)) : buAffinePoint τ scale z ∈ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1)

The affine parabolic map preserves the positive half-space cylinder when its image time interval stays below one.

theorem ESS.buAffinePoint_mem_halfClosure (τ scale : ℝ) (hτ : 0 ≤ τ) (hscale : 0 < scale) (hupper : τ + scale ^ 2 ≤ 1) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico 0 1) : buAffinePoint τ scale z ∈ {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico 0 1

The affine parabolic map also preserves the cylinder with its initial time face included.

theorem ESS.buAffinePoint_continuous (τ scale : ℝ) : Continuous (buAffinePoint τ scale)

The affine parabolic map is continuous.

theorem ESS.buAffineField_continuousOn (τ scale : ℝ) (hτ : 0 ≤ τ) (hscale : 0 < scale) (hupper : τ + scale ^ 2 ≤ 1) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hw : ContinuousOn w ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico 0 1)) : ContinuousOn (buAffineField τ scale w) ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico 0 1)

Continuity up to the initial time face transports under the affine map.

theorem ESS.buAffineField_initial_zero (τ scale : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hzero : ∀ (x : CKN.Foundation.Parabolic.Vec3), 0 < x 2 → w (x, τ) = 0) (hscale : 0 < scale) (y : CKN.Foundation.Parabolic.Vec3) (hy : 0 < y 2) : buAffineField τ scale w (y, 0) = 0

The affine field has the prescribed zero trace at normalized time zero.

theorem ESS.buAffineField_growth (M A τ scale : ℝ) (hscale : 0 < scale) (hA : M * scale ^ 2 ≤ A) (hτ : 0 ≤ τ) (hupper : τ + scale ^ 2 ≤ 1) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hgrowth : ∀ z ∈ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ≤ Real.exp (M * CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2)) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1)) : CKN.Foundation.Parabolic.vec3EuclideanNorm (buAffineField τ scale w z) ≤ Real.exp (A * CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2)

Gaussian growth is preserved when the rescaled exponent is bounded by the target exponent.