Extended rescaled data for short-time cells

The Gaussian averaging boxes near the top of the dyadic range extend slightly past normalized time one. The original field provides data up to normalized time three halves whenever the parabolic scale is small.

theorem ESS.bu_short_extended_source_interval (scale : ℝ) : Set.Ioo (-scale ^ 2 / 2 + scale ^ 2 * (1 / 2)) (-scale ^ 2 / 2 + scale ^ 2 * (3 / 2)) = Set.Ioo 0 (scale ^ 2)

The extended normalized interval maps to the physical interval from zero to scale².

theorem ESS.bu_short_extended_continuousOn (scale : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hcont : ContinuousOn w ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico 0 1)) : ContinuousOn (buAffineField (-scale ^ 2 / 2) scale w) ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico (1 / 2) (3 / 2))

The shifted field is continuous on the extended cylinder through its lower time face.

theorem ESS.bu_short_extended_weak_derivatives (scale : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (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 {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1) w Dw D2w Dtw) : CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (1 / 2) (3 / 2)) (buAffineField (-scale ^ 2 / 2) scale w) (buAffineDw (-scale ^ 2 / 2) scale Dw) (buAffineD2w (-scale ^ 2 / 2) scale D2w) (buAffineDtw (-scale ^ 2 / 2) scale Dtw)

Weak derivatives persist on the extended normalized interval.

theorem ESS.bu_short_extended_derivative_l2 (scale : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (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 {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 < ⊤) (K : Set CKN.Foundation.Parabolic.ParabolicPoint) : K ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (1 / 2) (3 / 2)) → Bornology.IsBounded K → ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in K, ‖buAffineDw (-scale ^ 2 / 2) scale Dw z‖ₑ ^ 2 + ‖buAffineD2w (-scale ^ 2 / 2) scale D2w z‖ₑ ^ 2 + ‖buAffineDtw (-scale ^ 2 / 2) scale Dtw z‖ₑ ^ 2 < ⊤

The derivative square integral is locally finite on the extended normalized interval.

theorem ESS.bu_short_extended_heat_ae_bound (scale c₁ : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hc₁ : 0 ≤ c₁) (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) (hineq : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1)), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2w Dtw z) ≤ c₁ * (√(CKN.spatialGradientSq w Dw z) + CKN.Foundation.Parabolic.vec3EuclideanNorm (w z))) : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (1 / 2) (3 / 2))), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector (buAffineD2w (-scale ^ 2 / 2) scale D2w) (buAffineDtw (-scale ^ 2 / 2) scale Dtw) z) ≤ c₁ * scale * (√(CKN.spatialGradientSq (buAffineField (-scale ^ 2 / 2) scale w) (buAffineDw (-scale ^ 2 / 2) scale Dw) z) + CKN.Foundation.Parabolic.vec3EuclideanNorm (buAffineField (-scale ^ 2 / 2) scale w z))

The weak heat inequality holds on the extended normalized interval with the scaled coefficient.