Rescaled data for the initial-time trace estimate

The unshifted parabolic rescaling has zero trace at time zero and retains the specified weak time derivative and local quadratic bounds on every bounded spatial ball in the half-space.

def ESS.buShortTraceBall (R : ℝ) : Set CKN.Foundation.Parabolic.Vec3

Bounded positive-half-space ball used to control the early cutoff error.

Equations

• ESS.buShortTraceBall R = CKN.euclideanBall 0 (2 * R) ∩ {y : CKN.Foundation.Parabolic.Vec3 | 0 < y 2}

theorem ESS.buShortTraceBall_geometry {R : ℝ} (hR : 0 < R) : IsOpen (buShortTraceBall R) ∧ MeasureTheory.volume (buShortTraceBall R) < ⊤ ∧ buShortTraceBall R ⊆ {y : CKN.Foundation.Parabolic.Vec3 | 0 < y 2}

The trace ball is open, has finite volume, and lies in the positive half-space.

theorem ESS.buShortTraceBall_cylinder_bounded {R : ℝ} (hR : 0 < R) : Bornology.IsBounded (CKN.spaceTimeSet (buShortTraceBall R) (Set.Ioo 0 1))

The full trace cylinder over a bounded ball is bounded in the parabolic metric.

theorem ESS.bu_short_trace_rescaled_data (scale R : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hR : 0 < R) (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) (hcont : ContinuousOn w ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico 0 1)) (hinit : ∀ (x : CKN.Foundation.Parabolic.Vec3), 0 < x 2 → w (x, 0) = 0) (hweak : CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1) w Dw D2w Dtw) (hL2 : ∀ S ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1), Bornology.IsBounded S → ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) : have B := buShortTraceBall R; have v := buAffineField 0 scale w; have Dv := buAffineDw 0 scale Dw; have D2v := buAffineD2w 0 scale D2w; have Dtv := buAffineDtw 0 scale Dtw; ContinuousOn v (CKN.spaceTimeSet B (Set.Ico 0 1)) ∧ (∀ x ∈ B, v (x, 0) = 0) ∧ CKN.HasSpaceTimeWeakDerivs B (Set.Ioo 0 1) v Dv D2v Dtv ∧ MeasureTheory.MemLp Dtv 2 ((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict (Set.Ioo 0 1)))

The unshifted rescaling satisfies all data required by the small-time trace estimate on the bounded half-space ball.