Vanishing from exponential decay in the positive phase

An exponential bound with the negative phase gap forces a continuous field to vanish at interior points of any compact positive-phase set.

theorem ESS.bu_short_zero_of_positive_phase_decay (scale : ℝ) (S : Set CKN.Foundation.Parabolic.ParabolicPoint) (hScompact : IsCompact S) (hSpositive : S ⊆ buShortPositivePhaseRegion scale) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hv : ContinuousOn v S) (C D a₀ : ℝ) (hD : 0 < D) (hbound : ∀ (a : ℝ), a₀ < a → ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in S, buShortShiftedWeight scale a q * CKN.Foundation.Parabolic.vec3EuclideanNorm (v q) ^ 2 ≤ C * Real.exp (-(a * D))) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ interior S) : v z = 0

If the weighted mass on a compact positive-phase region has the negative-phase decay rate at every large Carleman parameter, then the field vanishes at every interior point.