PartitionIntegral.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Gluing nonnegative cell estimates over a countable measurable partition.

theorem OAI.LipschitzHilbert.integral_le_of_partition line 18

Source documentation

Summable control on partition cells proves global integrability as well as the global estimate; no integrability of the left side is assumed.

theorem integral_le_of_partition (μ : Measure α) (s : ι → Set α)
    (hs : ∀ i, MeasurableSet (s i)) (hd : Pairwise (fun i j => Disjoint (s i) (s j)))
    (hcover : (⋃ i, s i) = Set.univ) (f g : α → ℝ) {C : ℝ}
    (hf0 : ∀ x, 0 ≤ f x) (hgint : Integrable g μ)
    (hf : ∀ i, IntegrableOn f (s i) μ)
    (hbound : ∀ i, (∫ x in s i, f x ∂μ) ≤ C * ∫ x in s i, g x ∂μ) :
    Integrable f μ ∧ (∫ x, f x ∂μ) ≤ C * ∫ x, g x ∂μ := by
…