Summation of local Gaussian-cell estimates

Real-valued integral summation for the finite space-time covers used in eq:bu-gaussian-collar.

theorem ESS.integral_le_sum_of_finite_cover {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (S : Set α) (I : Finset ι) (U : ι → Set α) (f : α → ℝ) (hf : MeasureTheory.Integrable f μ) (hfn : ∀ᵐ (x : α) ∂μ, 0 ≤ f x) (hS : MeasurableSet S) (hU : ∀ i ∈ I, MeasurableSet (U i)) (hcover : ∀ x ∈ S, ∃ i ∈ I, x ∈ U i) : ∫ (x : α) in S, f x ∂μ ≤ ∑ i ∈ I, ∫ (x : α) in U i, f x ∂μ

If a finite measurable family covers a set, its cell integrals dominate the integral of every nonnegative function over that set.

theorem ESS.integral_sum_le_of_cylinder_product_multiplicity {ι : Type u_1} {κ : Type u_2} (Y : Finset ι) (J : Finset κ) (B : ι → Set CKN.Foundation.Parabolic.Vec3) (T : κ → Set ℝ) (N K : ℕ) (f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hfn : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint), 0 ≤ f z) (hB : ∀ i ∈ Y, MeasurableSet (B i)) (hT : ∀ j ∈ J, MeasurableSet (T j)) (hspace : ∀ (y : CKN.Foundation.Parabolic.Vec3), (∑ i ∈ Y, if y ∈ B i then 1 else 0) ≤ N) (htime : ∀ (s : ℝ), (∑ j ∈ J, if s ∈ T j then 1 else 0) ≤ K) : ∑ p ∈ Y.product J, ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (B p.1) (T p.2), f z ≤ ↑(K * N) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), f z

Spatial and temporal multiplicity bounds multiply for finite product covers of parabolic cylinders.