Lebesgue integrals over an increasing family of sets

The Lebesgue integrals of a function f : α → ℝ≥0∞ over an increasing countable family of sets tend to its integral over their union. No measurability of f or of the sets is assumed. This is the ℝ≥0∞-valued counterpart of Mathlib's MeasureTheory.tendsto_setIntegral_of_monotone, and it computes integrals over unbounded domains by exhausting them with bounded pieces.

Main statements

• TauCeti.tendsto_setLIntegral_of_monotone: ∫⁻_{s i} f → ∫⁻_{⋃ i, s i} f for monotone s.
• TauCeti.setLIntegral_le_of_forall_inter_le: ∫_A g ≤ c when the integrals over the pieces A ∩ V n of an exhaustion V of A are eventually bounded by a family converging to c.

theorem TauCeti.tendsto_setLIntegral_of_monotone {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [Countable ι] [Preorder ι] [IsDirectedOrder ι] {f : α → ENNReal} {s : ι → Set α} (hs : Monotone s) : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : α) in s i, f x ∂μ) Filter.atTop (nhds (∫⁻ (x : α) in ⋃ (i : ι), s i, f x ∂μ))

Integrals over an exhaustion. The integrals of f over an increasing countable family of sets s i tend to its integral over their union.

theorem TauCeti.setLIntegral_le_of_forall_inter_le {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [Countable ι] [Preorder ι] [IsDirectedOrder ι] [Nonempty ι] {A : Set α} {V : ι → Set α} (hV : Monotone V) (hA : A ⊆ ⋃ (n : ι), V n) {g : α → ENNReal} {f : ι → ENNReal} {c : ENNReal} (hf : Filter.Tendsto f Filter.atTop (nhds c)) (h : ∀ᶠ (n : ι) in Filter.atTop, ∫⁻ (x : α) in A ∩ V n, g x ∂μ ≤ f n) : ∫⁻ (x : α) in A, g x ∂μ ≤ c

If the integrals of g over A ∩ V n, for an increasing family of sets V n covering A, indexed by a countable directed order, are eventually bounded by a family converging to c, then the integral of g over A is at most c.