Lebesgue integrals over a union #
The Lebesgue integral over the union of finitely many sets is at most the sum of the integrals over
the sets, without any disjointness or measurability assumption. This is the finite form of
MeasureTheory.lintegral_iUnion_le, and the subadditive counterpart of
MeasureTheory.lintegral_biUnion_finset. It is how a local estimate on finitely many open sets
covering a compact space becomes a global one.
Main statements #
TauCeti.lintegral_biUnion_finset_le:∫_{⋃ b ∈ s, t b} f ≤ ∑ b ∈ s, ∫_{t b} f.
theorem
TauCeti.lintegral_biUnion_finset_le
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
(s : Finset β)
(t : β → Set α)
(f : α → ENNReal)
:
The Lebesgue integral over a finite union is at most the sum of the integrals over the sets.