Recovering pointwise zero from quadratic mass

On the interior of a compact region, a continuous field with zero quadratic integral vanishes pointwise.

theorem ESS.bu_short_zero_of_compact_sq_integral_zero (S : Set CKN.Foundation.Parabolic.ParabolicPoint) (hScompact : IsCompact S) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hv : ContinuousOn v S) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ interior S) (hzero : ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in S, CKN.Foundation.Parabolic.vec3EuclideanNorm (v q) ^ 2 = 0) : v z = 0

Zero quadratic mass of a continuous vector field on a compact set forces vanishing at every interior point.

theorem ESS.bu_short_zero_of_base_weighted_integral_zero (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) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ interior S) (hzero : ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in S, buShortShiftedWeight scale 0 q * CKN.Foundation.Parabolic.vec3EuclideanNorm (v q) ^ 2 = 0) : v z = 0

Zero mass against the positive phase-independent weight forces a continuous field to vanish at interior points of the compact region.