Translating the initial-time trace strip

The shifted field used by the half-space Carleman estimate is the unshifted parabolic rescaling evaluated at time s - 1/2.

theorem ESS.bu_short_shifted_field_eq_unshifted (scale : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (y : CKN.Foundation.Parabolic.Vec3) (s : ℝ) : buAffineField (-scale ^ 2 / 2) scale w (y, s) = buAffineField 0 scale w (y, s - 1 / 2)

The shifted and unshifted parabolic rescalings differ by a translation of one half in the normalized time variable.

theorem ESS.bu_short_shifted_strip_lintegral (B : Set CKN.Foundation.Parabolic.Vec3) (ε : ℝ) (F : CKN.Foundation.Parabolic.Vec3 × ℝ → ENNReal) : ∫⁻ (s : ℝ) in Set.Ioc (1 / 2 + ε) (1 / 2 + 2 * ε), ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in B, F (x, s - 1 / 2) = ∫⁻ (t : ℝ) in Set.Ioc ε (2 * ε), ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in B, F (x, t)

A time translation carries the early strip in shifted coordinates to the initial strip in unshifted coordinates.

theorem ESS.bu_short_shifted_trace_strip_tendsto_zero (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 < ⊤) : Filter.Tendsto (fun (ε : ℝ) => (∫⁻ (s : ℝ) in Set.Ioc (1 / 2 + ε) (1 / 2 + 2 * ε), ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in buShortTraceBall R, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (buAffineField (-scale ^ 2 / 2) scale w (x, s)) ^ 2)) / ENNReal.ofReal ε ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

The shifted rescaling has vanishing normalized quadratic mass in its early-time strip on the bounded trace ball.