Unique continuation from an open zero region #
An open zero neighborhood around an interior point gives integral flatness after translating that point to the origin.
theorem
ESS.bu_short_uc_zero_from_open_set
(M τ δ c₁ R : ℝ)
(c : CKN.Foundation.Parabolic.Vec3)
(hτ : 0 < τ)
(hδ : 0 < δ)
(hδ1 : δ ≤ 1)
(hend : τ + δ ^ 2 * 2 < 1)
(hc₁ : 0 < c₁)
(hR : 0 < R)
(hball : CKN.Foundation.Parabolic.vec3Ball c R ⊆ {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2})
(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))
(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 < ⊤)
(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)))
(hgrowth :
∀ z ∈ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1),
CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ≤ Real.exp (M * CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2))
(U : Set CKN.Foundation.Parabolic.ParabolicPoint)
(hUopen : IsOpen U)
(hcenter : (δ • c, τ) ∈ U)
(hUzero : ∀ q ∈ U, w q = 0)
:
have W := ucScaledField c 1 (buAffineField τ δ w);
∀ y ∈ CKN.Foundation.Parabolic.vec3Ball 0 R, W (y, 0) = 0
A zero neighborhood at an interior point fills a half-space ball
at that time (lem:bu-small-time, thm:uc).