Integral flatness from Gaussian boxes #
Uniform Gaussian decay on nearby boxes yields vanishing of every integral order at their common spatial center.
theorem
ESS.uc_box_decay_implies_integral_flatness
(F : Finset CKN.Foundation.Parabolic.Vec3)
(hF : ∀ y ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 1), ∃ c ∈ F, y ∈ CKN.Foundation.Parabolic.vec3Ball c (1 / 2))
(hFpos : 0 < F.card)
(x : CKN.Foundation.Parabolic.Vec3)
(R T δ A b : ℝ)
(hδ : 0 < δ)
(hA : 0 ≤ A)
(hb : 0 < b)
(w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(hlocalInt :
∀ (r : ℝ),
0 < r →
r < δ →
MeasureTheory.IntegrableOn
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2)
(CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x r) (Set.Ioo 0 (r ^ 2))) MeasureTheory.volume)
(hslabInt :
∀ (r : ℝ),
0 < r →
r < δ →
∀ (n : ℕ),
MeasureTheory.IntegrableOn
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2)
(CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x r)
(Set.Ioo (3 / 5 * (3 / 4) ^ n * r ^ 2) (2 * (3 / 5 * (3 / 4) ^ n * r ^ 2))))
MeasureTheory.volume)
(hboxInt :
∀ (r : ℝ),
0 < r →
r < δ →
∀ (n : ℕ),
∀ c ∈ CKN.Foundation.Parabolic.vec3Ball x (2 * r),
MeasureTheory.IntegrableOn
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2)
(CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball c √(2 * (3 / 5 * (3 / 4) ^ n * r ^ 2)))
(Set.Ioo (3 / 5 * (3 / 4) ^ n * r ^ 2) (2 * (3 / 5 * (3 / 4) ^ n * r ^ 2))))
MeasureTheory.volume)
(hbox :
∀ (r : ℝ),
0 < r →
r < δ →
∀ (n : ℕ),
∀ c ∈ CKN.Foundation.Parabolic.vec3Ball x (2 * r),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball c √(2 * (3 / 5 * (3 / 4) ^ n * r ^ 2)))
(Set.Ioo (3 / 5 * (3 / 4) ^ n * r ^ 2) (2 * (3 / 5 * (3 / 4) ^ n * r ^ 2))), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2 ≤ A * Real.exp (-(b / (3 / 5 * (3 / 4) ^ n * r ^ 2))))
:
UCIntegralFlatness x R T w
Uniform Gaussian decay over all sufficiently small nearby boxes yields integral vanishing of every order at their common spatial center.