Gaussian control of one geometric time slab #
The finite spatial cover turns uniform Gaussian box bounds into a slab bound with geometric covering multiplicity.
theorem
ESS.uc_geometric_slab_integral_le
(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))
(x : CKN.Foundation.Parabolic.Vec3)
(r : ℝ)
(hr : 0 < r)
(n : ℕ)
(f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hf : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), 0 ≤ f z)
(A : ℝ)
(hA : 0 ≤ A)
(hSInt :
MeasureTheory.IntegrableOn f
(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 :
∀ c ∈ CKN.Foundation.Parabolic.vec3Ball x (2 * r),
MeasureTheory.IntegrableOn f
(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 :
∀ 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))), f z ≤ A)
:
Uniform bounds on Gaussian boxes control the corresponding local space-time slab.