Subtraction of Lebesgue integrals

In this file we first show that Lebesgue integrals can be subtracted with the expected results – ∫⁻ f - ∫⁻ g ≤ ∫⁻ (f - g), with equality if g ≤ f almost everywhere. Then we prove variants of the monotone convergence theorem that use this subtraction in their proofs.

theorem MeasureTheory.lintegral_sub' {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f g : α → ENNReal} (hg : AEMeasurable g μ) (hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤) (h_le : g ≤ᶠ[ae μ] f) : ∫⁻ (a : α), f a - g a ∂μ = ∫⁻ (a : α), f a ∂μ - ∫⁻ (a : α), g a ∂μ

theorem MeasureTheory.lintegral_sub {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f g : α → ENNReal} (hg : Measurable g) (hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤) (h_le : g ≤ᶠ[ae μ] f) : ∫⁻ (a : α), f a - g a ∂μ = ∫⁻ (a : α), f a ∂μ - ∫⁻ (a : α), g a ∂μ

theorem MeasureTheory.lintegral_sub_le' {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (f g : α → ENNReal) (hf : AEMeasurable f μ) : ∫⁻ (x : α), g x ∂μ - ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ

theorem MeasureTheory.lintegral_sub_le {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (f g : α → ENNReal) (hf : Measurable f) : ∫⁻ (x : α), g x ∂μ - ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ

theorem MeasureTheory.lintegral_iInf_ae {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f : ℕ → α → ENNReal} (h_meas : ∀ (n : ℕ), Measurable (f n)) (h_mono : ∀ (n : ℕ), f n.succ ≤ᶠ[ae μ] f n) (h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤) : ∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Monotone convergence theorem for nonincreasing sequences of functions.

theorem MeasureTheory.lintegral_iInf {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f : ℕ → α → ENNReal} (h_meas : ∀ (n : ℕ), Measurable (f n)) (h_anti : Antitone f) (h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤) : ∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Monotone convergence theorem for nonincreasing sequences of functions.

theorem MeasureTheory.lintegral_iInf' {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f : ℕ → α → ENNReal} (h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ) (h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun (i : ℕ) => f i a) (h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤) : ∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

theorem MeasureTheory.lintegral_iInf_directed_of_measurable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Countable β] {f : β → α → ENNReal} {μ : Measure α} (hμ : μ ≠ 0) (hf : ∀ (b : β), Measurable (f b)) (hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ⊤) (h_directed : Directed (fun (x1 x2 : α → ENNReal) => x1 ≥ x2) f) : ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ = ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ

Monotone convergence theorem for an infimum over a directed family and indexed by a countable type.

theorem MeasureTheory.lintegral_tendsto_of_tendsto_of_antitone {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f : ℕ → α → ENNReal} {F : α → ENNReal} (hf : ∀ (n : ℕ), AEMeasurable (f n) μ) (h_anti : ∀ᵐ (x : α) ∂μ, Antitone fun (n : ℕ) => f n x) (h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤) (h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (F x))) : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (x : α), f n x ∂μ) Filter.atTop (nhds (∫⁻ (x : α), F x ∂μ))

theorem MeasureTheory.exists_setLintegral_compl_lt {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f : α → ENNReal} (hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) : ∃ (s : Set α), MeasurableSet s ∧ μ s < ⊤ ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε

If f : α → ℝ≥0∞ has finite integral, then there exists a measurable set s of finite measure such that the integral of f over sᶜ is less than a given positive number.

Also used to prove an Lᵖ-norm version in MeasureTheory.MemLp.exists_eLpNorm_indicator_compl_le.

theorem MeasureTheory.exists_measurable_le_setLintegral_eq_of_integrable {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f : α → ENNReal} (hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤) : ∃ (g : α → ENNReal), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), MeasurableSet s → ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ

For any function f : α → ℝ≥0∞, there exists a measurable function g ≤ f with the same integral over any measurable set.