OAI/Geometry/RCD/Metric/FiniteCoverIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.integral_le_sum_cover line 17

   Source documentation

   Integrate a nonnegative function over a finite cover, allowing overlap.

   theorem integral_le_sum_cover (s : Finset I) (A : I → Set X) (hA : ∀ i ∈ s, MeasurableSet (A i))
       {Ω : Set X} (hΩ : MeasurableSet Ω) (hcover : Ω ⊆ ⋃ i ∈ s, A i)
       {f : X → ℝ} (hf : Integrable f μ) (hpos : ∀ x, 0 ≤ f x) :
       (∫ x in Ω, f x ∂μ) ≤ ∑ i ∈ s, ∫ x in A i, f x ∂μ := by
   …

2. theorem OAI.RegularPointCoordinates.sum_integral_le_overlap line 42

   Source documentation

   A bound on overlap controls the sum of local integrals by the global integral, with precisely the same multiplicity constant.

   theorem sum_integral_le_overlap (s : Finset I) (A : I → Set X)
       (hA : ∀ i ∈ s, MeasurableSet (A i)) (N : ℕ)
       (hoverlap : ∀ x, (s.filter (fun i => x ∈ A i)).card ≤ N)
       {f : X → ℝ} (hf : Integrable f μ) (hpos : ∀ x, 0 ≤ f x) :
       (∑ i ∈ s, ∫ x in A i, f x ∂μ) ≤ N * ∫ x, f x ∂μ := by
   …