Consequences of dominated convergence for Lebesgue integrals

A function f : α → ℝ≥0∞ of finite Lebesgue integral exceeds a large constant M only by an amount of small integral: ∫⁻ x, f x - M ∂μ → 0 as M → ∞. This is dominated convergence with the bound f, since f x - M vanishes for M ≥ f x and f is almost everywhere finite.

The file also records a squeeze principle: if f n ≤ g n + h n and the integrals of g n and h n tend to 0, so does the integral of f n; and the reverse Fatou lemma for integrals over sets: the integrals of a function of finite integral over measurable sets s n have limit superior at most its integral over limsup s n, the set of points lying in infinitely many s n.

Bounded real coefficients converging almost everywhere preserve L¹ convergence of vector-valued sequences. This lets products pass to the limit when the coefficient convergence is pointwise and the vector-valued factor converges only in L¹.

Main statements

• TauCeti.tendsto_lintegral_tsub_atTop: the integral of the excess of f over the constant M tends to 0 as M → ∞.
• TauCeti.tendsto_lintegral_zero_of_le_add: the integral of a function bounded by the sum of two functions with integrals tending to 0 tends to 0.
• TauCeti.tendsto_lintegral_enorm_smul_sub: bounded, almost everywhere convergent real coefficients preserve L¹ convergence in any real normed space.
• TauCeti.limsup_setLIntegral_le: limsup ∫⁻_{s n} f ≤ ∫⁻_{limsup s n} f when the s n lie in a set over which f has finite integral.

theorem TauCeti.tendsto_lintegral_tsub_atTop {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) (hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤) : Filter.Tendsto (fun (M : NNReal) => ∫⁻ (x : α), f x - ↑M ∂μ) Filter.atTop (nhds 0)

Uniformly small tails. If f : α → ℝ≥0∞ is almost everywhere measurable with finite Lebesgue integral, then the integral of its excess f x - M over a finite level M tends to 0 as M → ∞.

theorem TauCeti.tendsto_lintegral_zero_of_le_add {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : Type u_2} {l : Filter ι} {f g h : ι → α → ENNReal} (hfgh : ∀ (i : ι) (x : α), f i x ≤ g i x + h i x) (hg : ∀ (i : ι), AEMeasurable (g i) μ) (hgt : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : α), g i x ∂μ) l (nhds 0)) (hht : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : α), h i x ∂μ) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : α), f i x ∂μ) l (nhds 0)

If f n ≤ g n + h n pointwise, g n is almost everywhere measurable, and the Lebesgue integrals of g n and h n tend to 0, then so do those of f n.

theorem TauCeti.tendsto_lintegral_enorm_smul_sub {α : Type u_1} [MeasurableSpace α] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {ν : MeasureTheory.Measure α} {M : NNReal} {c : ℕ → α → ℝ} {c₀ : α → ℝ} {g : ℕ → α → E} {g₀ : α → E} (hc : ∀ (i : ℕ), MeasureTheory.AEStronglyMeasurable (c i) ν) (hg : ∀ (i : ℕ), MeasureTheory.AEStronglyMeasurable (g i) ν) (hg₀ : MeasureTheory.AEStronglyMeasurable g₀ ν) (hcM : ∀ (i : ℕ), ∀ᵐ (x : α) ∂ν, ‖c i x‖₊ ≤ M) (hlim : ∀ᵐ (x : α) ∂ν, Filter.Tendsto (fun (i : ℕ) => c i x) Filter.atTop (nhds (c₀ x))) (hg₀int : ∫⁻ (x : α), ‖g₀ x‖ₑ ∂ν ≠ ⊤) (hgg : Filter.Tendsto (fun (i : ℕ) => ∫⁻ (x : α), ‖g i x - g₀ x‖ₑ ∂ν) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (i : ℕ) => ∫⁻ (x : α), ‖c i x • g i x - c₀ x • g₀ x‖ₑ ∂ν) Filter.atTop (nhds 0)

If bounded coefficients c i converge almost everywhere to c₀ and g i → g₀ in L¹, then c i • g i → c₀ • g₀ in L¹. The functions take values in any real normed space.

theorem TauCeti.limsup_setLIntegral_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal} {s : ℕ → Set α} {t : Set α} (hf : Measurable f) (hs : ∀ (n : ℕ), MeasurableSet (s n)) (hst : ∀ (n : ℕ), s n ⊆ t) (ht : ∫⁻ (x : α) in t, f x ∂μ ≠ ⊤) : Filter.limsup (fun (n : ℕ) => ∫⁻ (x : α) in s n, f x ∂μ) Filter.atTop ≤ ∫⁻ (x : α) in Filter.limsup s Filter.atTop, f x ∂μ

The reverse Fatou lemma for integrals over sets. Let f be measurable, let the sets s n be measurable and contained in a set t over which f has finite integral. Then the limit superior of the integrals of f over s n is at most the integral of f over limsup s n, the set of points that lie in s n for infinitely many n.