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_iInf
{α : Type u_1}
[MeasurableSpace α]
{μ : Measure α}
{f : ℕ → α → ENNReal}
(h_meas : ∀ (n : ℕ), Measurable (f n))
(h_anti : Antitone f)
(h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤)
:
Monotone convergence theorem for nonincreasing sequences of functions.
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)
:
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)
:
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.