One unique-continuation step

At an interior center with integral flatness and zero initial trace, the Gaussian estimate propagates both properties through its output ball.

theorem ESS.uc_one_center_propagation (R T c₁ : ℝ) (hT : 0 < T) (hc₁ : 0 < c₁) (x₀ : CKN.Foundation.Parabolic.Vec3) (hx₀ : x₀ ∈ CKN.Foundation.Parabolic.vec3Ball 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 (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ico 0 T)) (hweak : CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ioo 0 T) w Dw D2w Dtw) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ioo 0 T), ‖w z‖ₑ ^ 2 + ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) (hineq : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ioo 0 T)), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2w Dtw z) ≤ c₁ * (CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) + √(CKN.spatialGradientSq w Dw z))) (hzero : w (x₀, 0) = 0) (hflat : UCIntegralFlatness x₀ (R - CKN.Foundation.Parabolic.vec3EuclideanNorm x₀) (min T 1) w) (y : CKN.Foundation.Parabolic.Vec3) : y ∈ CKN.Foundation.Parabolic.vec3Ball x₀ (ucRadiusFraction * (R - CKN.Foundation.Parabolic.vec3EuclideanNorm x₀)) → w (y, 0) = 0 ∧ UCIntegralFlatness y (R - CKN.Foundation.Parabolic.vec3EuclideanNorm x₀) (min T 1) w

Integral flatness and the zero trace propagate through one Gaussian spatial reach.