# 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.

source
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 ∂μ
source
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 ∂μ
source
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 ∂μ
source
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 ∂μ
source
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.

source
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.

source
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 ∂μ
source
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.

source
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 ∂μ))
source
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`.

source
@[deprecated MeasureTheory.exists_setLIntegral_compl_lt (since := "2025-04-22")]
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 ∂μ < ε

Alias of `MeasureTheory.exists_setLIntegral_compl_lt`.

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`.

source
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.

source
@[deprecated MeasureTheory.exists_measurable_le_setLIntegral_eq_of_integrable (since := "2025-04-22")]
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 ∂μ

Alias of `MeasureTheory.exists_measurable_le_setLIntegral_eq_of_integrable`.

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