Neighborhood geometry for Gaussian boxes #
Small local cylinders and every geometric covering box remain inside a fixed cylinder around their common spatial center.
theorem
ESS.uc_neighborhood_boxes_subset
(x : CKN.Foundation.Parabolic.Vec3)
(L S r : ℝ)
(hL : 0 < L)
(hS : 0 < S)
(hr : 0 < r)
(hrL : r < L / 4)
(hrS : r < √(S / 2))
(n : ℕ)
:
have U := CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x L) (Set.Ioo 0 S);
CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x r) (Set.Ioo 0 (r ^ 2)) ⊆ U ∧ 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))) ⊆
U ∧ ∀ c ∈ CKN.Foundation.Parabolic.vec3Ball x (2 * r),
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))) ⊆
U
Local cylinders, geometric slabs, and nearby Gaussian boxes stay inside a fixed positive-time neighborhood.
theorem
ESS.uc_gaussian_neighborhood_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 L S δ A b : ℝ)
(hL : 0 < L)
(hS : 0 < S)
(hδ : 0 < δ)
(hδL : δ ≤ L / 4)
(hδS : δ ≤ √(S / 2))
(hA : 0 ≤ A)
(hb : 0 < b)
(w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(hInt :
MeasureTheory.IntegrableOn
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2)
(CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x L) (Set.Ioo 0 S)) 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
An integrable neighborhood supplies the local integrability hypotheses for Gaussian box propagation.