Short-time parabolic coordinates

The initial physical interval is placed at the lower face of the shifted half-space Carleman cylinder in lem:bu-small-time.

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

The shifted parabolic map sends the normalized interval (1/2,1) onto the initial physical interval (0,scale²/2).

theorem ESS.bu_short_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) 1) (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 transfer to the shifted half-space cylinder.

theorem ESS.bu_short_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) 1) → 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 local quadratic derivative bound persists on the shifted half-space cylinder.

theorem ESS.bu_short_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) 1)), 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 differential inequality in the shifted cylinder has coefficient c₁ * scale.