Vanishing in the positive phase #
The negative-phase estimate forces the shifted field to vanish wherever the Carleman phase is positive.
theorem
ESS.bu_short_positive_phase_zero :
∃ (a₀ : ℝ) (c : ℝ),
0 < a₀ ∧ 0 < c ∧ ∀ (M scale c₁ C₁ C₂ : ℝ),
0 < M →
0 < scale →
scale ≤ 1 →
0 ≤ c₁ →
0 ≤ C₁ →
(∀ (scale y : ℝ), |deriv (deriv (buShortNormalCutoff scale)) y| ≤ C₁) →
0 ≤ C₂ →
(∀ (x : ℝ), |deriv (deriv CKN.smoothTransitionProfile) x| ≤ C₂) →
c * 36 * (c₁ * scale) ^ 2 ≤ 1 / 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),
ContinuousOn w ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico 0 1) →
(∀ (x : CKN.Foundation.Parabolic.Vec3), 0 < x 2 → w (x, 0) = 0) →
CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1) w
Dw D2w Dtw →
(∀ 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 < ⊤) →
(∀ᵐ (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.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)) →
MeasureTheory.IntegrableOn (buShortTangentialDensity scale w Dw)
(buShortWideGapRegion scale) MeasureTheory.volume →
(∀ (a : ℝ),
max a₀ 1 < a →
MeasureTheory.IntegrableOn
(buShortWeightedPolynomialDensity scale a w Dw)
(buShortHighStrip scale) MeasureTheory.volume) →
(∀ (a : ℝ),
max a₀ 1 < a →
MeasureTheory.IntegrableOn (buShortWeightedDensity scale a w Dw)
(buShortHighStrip scale) MeasureTheory.volume) →
∀ z ∈ buShortPositivePhaseRegion scale,
buAffineField (-scale ^ 2 / 2) scale w z = 0
The shifted field vanishes in the positive-phase region once its Gaussian energy densities are integrable at each fixed parameter.