# Documentation

Mathlib.MeasureTheory.Integral.Lebesgue

# Lower Lebesgue integral for ℝ≥0∞-valued functions #

We define the lower Lebesgue integral of an ℝ≥0∞-valued function.

## Notation #

We introduce the following notation for the lower Lebesgue integral of a function f : α → ℝ≥0∞.

• ∫⁻ x, f x ∂μ: integral of a function f : α → ℝ≥0∞ with respect to a measure μ;
• ∫⁻ x, f x: integral of a function f : α → ℝ≥0∞ with respect to the canonical measure volume on α;
• ∫⁻ x in s, f x ∂μ: integral of a function f : α → ℝ≥0∞ over a set s with respect to a measure μ, defined as ∫⁻ x, f x ∂(μ.restrict s);
• ∫⁻ x in s, f x: integral of a function f : α → ℝ≥0∞ over a set s with respect to the canonical measure volume, defined as ∫⁻ x, f x ∂(volume.restrict s).
theorem MeasureTheory.lintegral_def {α : Type u_5} :
∀ {x : } (μ : ) (f : αENNReal), = ⨆ (g : ) (_ : g f),
@[irreducible]
def MeasureTheory.lintegral {α : Type u_5} :
{x : } → (αENNReal) → ENNReal

The lower Lebesgue integral of a function f with respect to a measure μ.

Instances For

In the notation for integrals, an expression like ∫⁻ x, g ‖x‖ ∂μ will not be parsed correctly, and needs parentheses. We do not set the binding power of r to 0, because then ∫⁻ x, f x = 0 will be parsed incorrectly.

Instances For

The lower Lebesgue integral of a function f with respect to a measure μ.

Instances For
Instances For

The lower Lebesgue integral of a function f with respect to a measure μ.

Instances For

The lower Lebesgue integral of a function f with respect to a measure μ.

Instances For

The lower Lebesgue integral of a function f with respect to a measure μ.

Instances For
Instances For
theorem MeasureTheory.SimpleFunc.lintegral_eq_lintegral {α : Type u_1} {m : } (f : ) (μ : ) :
∫⁻ (a : α), f aμ =
theorem MeasureTheory.lintegral_mono' {α : Type u_1} {m : } ⦃μ : ⦃ν : (hμν : μ ν) ⦃f : αENNReal ⦃g : αENNReal (hfg : f g) :
∫⁻ (a : α), f aμ ∫⁻ (a : α), g aν
theorem MeasureTheory.lintegral_mono {α : Type u_1} {m : } {μ : } ⦃f : αENNReal ⦃g : αENNReal (hfg : f g) :
∫⁻ (a : α), f aμ ∫⁻ (a : α), g aμ
theorem MeasureTheory.lintegral_mono_nnreal {α : Type u_1} {m : } {μ : } {f : αNNReal} {g : αNNReal} (h : f g) :
∫⁻ (a : α), ↑(f a)μ ∫⁻ (a : α), ↑(g a)μ
theorem MeasureTheory.iSup_lintegral_measurable_le_eq_lintegral {α : Type u_1} {m : } {μ : } (f : αENNReal) :
⨆ (g : αENNReal) (_ : ) (_ : g f), ∫⁻ (a : α), g aμ = ∫⁻ (a : α), f aμ
theorem MeasureTheory.lintegral_mono_set {α : Type u_1} :
∀ {x : } ⦃μ : ⦄ {s t : Set α} {f : αENNReal}, s t∫⁻ (x : α) in s, f xμ ∫⁻ (x : α) in t, f xμ
theorem MeasureTheory.lintegral_mono_set' {α : Type u_1} :
∀ {x : } ⦃μ : ⦄ {s t : Set α} {f : αENNReal}, ∫⁻ (x : α) in s, f xμ ∫⁻ (x : α) in t, f xμ
theorem MeasureTheory.monotone_lintegral {α : Type u_1} :
∀ {x : } (μ : ),
@[simp]
theorem MeasureTheory.lintegral_const {α : Type u_1} {m : } {μ : } (c : ENNReal) :
∫⁻ (x : α), cμ = c * μ Set.univ
theorem MeasureTheory.lintegral_zero {α : Type u_1} {m : } {μ : } :
∫⁻ (x : α), 0μ = 0
theorem MeasureTheory.lintegral_zero_fun {α : Type u_1} {m : } {μ : } :
theorem MeasureTheory.lintegral_one {α : Type u_1} {m : } {μ : } :
∫⁻ (x : α), 1μ = μ Set.univ
theorem MeasureTheory.set_lintegral_const {α : Type u_1} {m : } {μ : } (s : Set α) (c : ENNReal) :
∫⁻ (x : α) in s, cμ = c * μ s
theorem MeasureTheory.set_lintegral_one {α : Type u_1} {m : } {μ : } (s : Set α) :
∫⁻ (x : α) in s, 1μ = μ s
theorem MeasureTheory.set_lintegral_const_lt_top {α : Type u_1} {m : } {μ : } (s : Set α) {c : ENNReal} (hc : c ) :
∫⁻ (x : α) in s, cμ <
theorem MeasureTheory.lintegral_const_lt_top {α : Type u_1} {m : } {μ : } {c : ENNReal} (hc : c ) :
∫⁻ (x : α), cμ <
theorem MeasureTheory.exists_measurable_le_lintegral_eq {α : Type u_1} {m : } (μ : ) (f : αENNReal) :
g, g f ∫⁻ (a : α), f aμ = ∫⁻ (a : α), g aμ

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

theorem MeasureTheory.lintegral_eq_nnreal {α : Type u_1} {m : } (f : αENNReal) (μ : ) :
∫⁻ (a : α), f aμ = ⨆ (φ : ) (_ : ∀ (x : α), ↑(φ x) f x),

∫⁻ a in s, f a ∂μ is defined as the supremum of integrals of simple functions φ : α →ₛ ℝ≥0∞ such that φ ≤ f. This lemma says that it suffices to take functions φ : α →ₛ ℝ≥0.

theorem MeasureTheory.exists_simpleFunc_forall_lintegral_sub_lt_of_pos {α : Type u_1} {m : } {μ : } {f : αENNReal} (h : ∫⁻ (x : α), f xμ ) {ε : ENNReal} (hε : ε 0) :
φ, (∀ (x : α), ↑(φ x) f x) ∀ (ψ : ), (∀ (x : α), ↑(ψ x) f x) →
theorem MeasureTheory.iSup_lintegral_le {α : Type u_1} {m : } {μ : } {ι : Sort u_5} (f : ιαENNReal) :
⨆ (i : ι), ∫⁻ (a : α), f i aμ ∫⁻ (a : α), ⨆ (i : ι), f i aμ
theorem MeasureTheory.iSup₂_lintegral_le {α : Type u_1} {m : } {μ : } {ι : Sort u_5} {ι' : ιSort u_6} (f : (i : ι) → ι' iαENNReal) :
⨆ (i : ι) (j : ι' i), ∫⁻ (a : α), f i j aμ ∫⁻ (a : α), ⨆ (i : ι) (j : ι' i), f i j aμ
theorem MeasureTheory.le_iInf_lintegral {α : Type u_1} {m : } {μ : } {ι : Sort u_5} (f : ιαENNReal) :
∫⁻ (a : α), ⨅ (i : ι), f i aμ ⨅ (i : ι), ∫⁻ (a : α), f i aμ
theorem MeasureTheory.le_iInf₂_lintegral {α : Type u_1} {m : } {μ : } {ι : Sort u_5} {ι' : ιSort u_6} (f : (i : ι) → ι' iαENNReal) :
∫⁻ (a : α), ⨅ (i : ι) (h : ι' i), f i h aμ ⨅ (i : ι) (h : ι' i), ∫⁻ (a : α), f i h aμ
theorem MeasureTheory.lintegral_mono_ae {α : Type u_1} {m : } {μ : } {f : αENNReal} {g : αENNReal} (h : ∀ᵐ (a : α) ∂μ, f a g a) :
∫⁻ (a : α), f aμ ∫⁻ (a : α), g aμ
theorem MeasureTheory.set_lintegral_mono_ae {α : Type u_1} {m : } {μ : } {s : Set α} {f : αENNReal} {g : αENNReal} (hf : ) (hg : ) (hfg : ∀ᵐ (x : α) ∂μ, x sf x g x) :
∫⁻ (x : α) in s, f xμ ∫⁻ (x : α) in s, g xμ
theorem MeasureTheory.set_lintegral_mono {α : Type u_1} {m : } {μ : } {s : Set α} {f : αENNReal} {g : αENNReal} (hf : ) (hg : ) (hfg : ∀ (x : α), x sf x g x) :
∫⁻ (x : α) in s, f xμ ∫⁻ (x : α) in s, g xμ
theorem MeasureTheory.set_lintegral_mono_ae' {α : Type u_1} {m : } {μ : } {s : Set α} {f : αENNReal} {g : αENNReal} (hs : ) (hfg : ∀ᵐ (x : α) ∂μ, x sf x g x) :
∫⁻ (x : α) in s, f xμ ∫⁻ (x : α) in s, g xμ
theorem MeasureTheory.set_lintegral_mono' {α : Type u_1} {m : } {μ : } {s : Set α} {f : αENNReal} {g : αENNReal} (hs : ) (hfg : ∀ (x : α), x sf x g x) :
∫⁻ (x : α) in s, f xμ ∫⁻ (x : α) in s, g xμ
theorem MeasureTheory.lintegral_congr_ae {α : Type u_1} {m : } {μ : } {f : αENNReal} {g : αENNReal} (h : ) :
∫⁻ (a : α), f aμ = ∫⁻ (a : α), g aμ
theorem MeasureTheory.lintegral_congr {α : Type u_1} {m : } {μ : } {f : αENNReal} {g : αENNReal} (h : ∀ (a : α), f a = g a) :
∫⁻ (a : α), f aμ = ∫⁻ (a : α), g aμ
theorem MeasureTheory.set_lintegral_congr {α : Type u_1} {m : } {μ : } {f : αENNReal} {s : Set α} {t : Set α} (h : ) :
∫⁻ (x : α) in s, f xμ = ∫⁻ (x : α) in t, f xμ
theorem MeasureTheory.set_lintegral_congr_fun {α : Type u_1} {m : } {μ : } {f : αENNReal} {g : αENNReal} {s : Set α} (hs : ) (hfg : ∀ᵐ (x : α) ∂μ, x sf x = g x) :
∫⁻ (x : α) in s, f xμ = ∫⁻ (x : α) in s, g xμ
theorem MeasureTheory.lintegral_ofReal_le_lintegral_nnnorm {α : Type u_1} {m : } {μ : } (f : α) :
∫⁻ (x : α), ENNReal.ofReal (f x)μ ∫⁻ (x : α), f x‖₊μ
theorem MeasureTheory.lintegral_nnnorm_eq_of_ae_nonneg {α : Type u_1} {m : } {μ : } {f : α} (h_nonneg : ) :
∫⁻ (x : α), f x‖₊μ = ∫⁻ (x : α), ENNReal.ofReal (f x)μ
theorem MeasureTheory.lintegral_nnnorm_eq_of_nonneg {α : Type u_1} {m : } {μ : } {f : α} (h_nonneg : 0 f) :
∫⁻ (x : α), f x‖₊μ = ∫⁻ (x : α), ENNReal.ofReal (f x)μ
theorem MeasureTheory.lintegral_iSup {α : Type u_1} {m : } {μ : } {f : αENNReal} (hf : ∀ (n : ), Measurable (f n)) (h_mono : ) :
∫⁻ (a : α), ⨆ (n : ), f n aμ = ⨆ (n : ), ∫⁻ (a : α), f n aμ

Monotone convergence theorem -- sometimes called Beppo-Levi convergence. See lintegral_iSup_directed for a more general form.

theorem MeasureTheory.lintegral_iSup' {α : Type u_1} {m : } {μ : } {f : αENNReal} (hf : ∀ (n : ), AEMeasurable (f n)) (h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x) :
∫⁻ (a : α), ⨆ (n : ), f n aμ = ⨆ (n : ), ∫⁻ (a : α), f n aμ

Monotone convergence theorem -- sometimes called Beppo-Levi convergence. Version with ae_measurable functions.

theorem MeasureTheory.lintegral_tendsto_of_tendsto_of_monotone {α : Type u_1} {m : } {μ : } {f : αENNReal} {F : αENNReal} (hf : ∀ (n : ), AEMeasurable (f n)) (h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x) (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μ))

Monotone convergence theorem expressed with limits

theorem MeasureTheory.lintegral_eq_iSup_eapprox_lintegral {α : Type u_1} {m : } {μ : } {f : αENNReal} (hf : ) :
∫⁻ (a : α), f aμ = ⨆ (n : ),
theorem MeasureTheory.exists_pos_set_lintegral_lt_of_measure_lt {α : Type u_1} {m : } {μ : } {f : αENNReal} (h : ∫⁻ (x : α), f xμ ) {ε : ENNReal} (hε : ε 0) :
δ, δ > 0 ∀ (s : Set α), μ s < δ∫⁻ (x : α) in s, f xμ < ε

If f has finite integral, then ∫⁻ x in s, f x ∂μ is absolutely continuous in s: it tends to zero as μ s tends to zero. This lemma states states this fact in terms of ε and δ.

theorem MeasureTheory.tendsto_set_lintegral_zero {α : Type u_1} {m : } {μ : } {ι : Type u_5} {f : αENNReal} (h : ∫⁻ (x : α), f xμ ) {l : } {s : ιSet α} (hl : Filter.Tendsto (μ s) l (nhds 0)) :
Filter.Tendsto (fun i => ∫⁻ (x : α) in s i, f xμ) l (nhds 0)

If f has finite integral, then ∫⁻ x in s, f x ∂μ is absolutely continuous in s: it tends to zero as μ s tends to zero.

theorem MeasureTheory.le_lintegral_add {α : Type u_1} {m : } {μ : } (f : αENNReal) (g : αENNReal) :
∫⁻ (a : α), f aμ + ∫⁻ (a : α), g aμ ∫⁻ (a : α), f a + g aμ

The sum of the lower Lebesgue integrals of two functions is less than or equal to the integral of their sum. The other inequality needs one of these functions to be (a.e.-)measurable.

theorem MeasureTheory.lintegral_add_aux {α : Type u_1} {m : } {μ : } {f : αENNReal} {g : αENNReal} (hf : ) (hg : ) :
∫⁻ (a : α), f a + g aμ = ∫⁻ (a : α), f aμ + ∫⁻ (a : α), g aμ
@[simp]
theorem MeasureTheory.lintegral_add_left {α : Type u_1} {m : } {μ : } {f : αENNReal} (hf : ) (g : αENNReal) :
∫⁻ (a : α), f a + g aμ = ∫⁻ (a : α), f aμ + ∫⁻ (a : α), g aμ

If f g : α → ℝ≥0∞ are two functions and one of them is (a.e.) measurable, then the Lebesgue integral of f + g equals the sum of integrals. This lemma assumes that f is integrable, see also MeasureTheory.lintegral_add_right and primed versions of these lemmas.

theorem MeasureTheory.lintegral_add_left' {α : Type u_1} {m : } {μ : } {f : αENNReal} (hf : ) (g : αENNReal) :
∫⁻ (a : α), f a + g aμ = ∫⁻ (a : α), f aμ + ∫⁻ (a : α), g aμ
theorem MeasureTheory.lintegral_add_right' {α : Type u_1} {m : } {μ : } (f : αENNReal) {g : αENNReal} (hg : ) :
∫⁻ (a : α), f a + g aμ = ∫⁻ (a : α), f aμ + ∫⁻ (a : α), g aμ
@[simp]
theorem MeasureTheory.lintegral_add_right {α : Type u_1} {m : } {μ : } (f : αENNReal) {g : αENNReal} (hg : ) :
∫⁻ (a : α), f a + g aμ = ∫⁻ (a : α), f aμ + ∫⁻ (a : α), g aμ

If f g : α → ℝ≥0∞ are two functions and one of them is (a.e.) measurable, then the Lebesgue integral of f + g equals the sum of integrals. This lemma assumes that g is integrable, see also MeasureTheory.lintegral_add_left and primed versions of these lemmas.

@[simp]
theorem MeasureTheory.lintegral_smul_measure {α : Type u_1} {m : } {μ : } (c : ENNReal) (f : αENNReal) :
∫⁻ (a : α), f ac μ = c * ∫⁻ (a : α), f aμ
@[simp]
theorem MeasureTheory.lintegral_sum_measure {α : Type u_1} {m : } {ι : Type u_5} (f : αENNReal) (μ : ) :
∫⁻ (a : α), f a = ∑' (i : ι), ∫⁻ (a : α), f aμ i
theorem MeasureTheory.hasSum_lintegral_measure {α : Type u_1} {ι : Type u_5} :
∀ {x : } (f : αENNReal) (μ : ), HasSum (fun i => ∫⁻ (a : α), f aμ i) (∫⁻ (a : α), f a)
@[simp]
theorem MeasureTheory.lintegral_add_measure {α : Type u_1} {m : } (f : αENNReal) (μ : ) (ν : ) :
∫⁻ (a : α), f a ∂(μ + ν) = ∫⁻ (a : α), f aμ + ∫⁻ (a : α), f aν
@[simp]
theorem MeasureTheory.lintegral_finset_sum_measure {α : Type u_1} {ι : Type u_5} {m : } (s : ) (f : αENNReal) (μ : ) :
(∫⁻ (a : α), f aFinset.sum s fun i => μ i) = Finset.sum s fun i => ∫⁻ (a : α), f aμ i
@[simp]
theorem MeasureTheory.lintegral_zero_measure {α : Type u_1} {m : } (f : αENNReal) :
∫⁻ (a : α), f a0 = 0
theorem MeasureTheory.set_lintegral_empty {α : Type u_1} {m : } {μ : } (f : αENNReal) :
∫⁻ (x : α) in , f xμ = 0
theorem MeasureTheory.set_lintegral_univ {α : Type u_1} {m : } {μ : } (f : αENNReal) :
∫⁻ (x : α) in Set.univ, f xμ = ∫⁻ (x : α), f xμ
theorem MeasureTheory.set_lintegral_measure_zero {α : Type u_1} {m : } {μ : } (s : Set α) (f : αENNReal) (hs' : μ s = 0) :
∫⁻ (x : α) in s, f xμ = 0
theorem MeasureTheory.lintegral_finset_sum' {α : Type u_1} {β : Type u_2} {m : } {μ : } (s : ) {f : βαENNReal} (hf : ∀ (b : β), b sAEMeasurable (f b)) :
∫⁻ (a : α), Finset.sum s fun b => f b aμ = Finset.sum s fun b => ∫⁻ (a : α), f b aμ
theorem MeasureTheory.lintegral_finset_sum {α : Type u_1} {β : Type u_2} {m : } {μ : } (s : ) {f : βαENNReal} (hf : ∀ (b : β), b sMeasurable (f b)) :
∫⁻ (a : α), Finset.sum s fun b => f b aμ = Finset.sum s fun b => ∫⁻ (a : α), f b aμ
@[simp]
theorem MeasureTheory.lintegral_const_mul {α : Type u_1} {m : } {μ : } (r : ENNReal) {f : αENNReal} (hf : ) :
∫⁻ (a : α), r * f aμ = r * ∫⁻ (a : α), f aμ
theorem MeasureTheory.lintegral_const_mul'' {α : Type u_1} {m : } {μ : } (r : ENNReal) {f : αENNReal} (hf : ) :
∫⁻ (a : α), r * f aμ = r * ∫⁻ (a : α), f aμ
theorem MeasureTheory.lintegral_const_mul_le {α : Type u_1} {m : } {μ : } (r : ENNReal) (f : αENNReal) :
r * ∫⁻ (a : α), f aμ ∫⁻ (a : α), r * f aμ
theorem MeasureTheory.lintegral_const_mul' {α : Type u_1} {m : } {μ : } (r : ENNReal) (f : αENNReal) (hr : r ) :
∫⁻ (a : α), r * f aμ = r * ∫⁻ (a : α), f aμ
theorem MeasureTheory.lintegral_mul_const {α : Type u_1} {m : } {μ : } (r : ENNReal) {f : αENNReal} (hf : ) :
∫⁻ (a : α), f a * rμ = (∫⁻ (a : α), f aμ) * r
theorem MeasureTheory.lintegral_mul_const'' {α : Type u_1} {m : } {μ : } (r : ENNReal) {f : αENNReal} (hf : ) :
∫⁻ (a : α), f a * rμ = (∫⁻ (a : α), f aμ) * r
theorem MeasureTheory.lintegral_mul_const_le {α : Type u_1} {m : } {μ : } (r : ENNReal) (f : αENNReal) :
(∫⁻ (a : α), f aμ) * r ∫⁻ (a : α), f a * rμ
theorem MeasureTheory.lintegral_mul_const' {α : Type u_1} {m : } {μ : } (r : ENNReal) (f : αENNReal) (hr : r ) :
∫⁻ (a : α), f a * rμ = (∫⁻ (a : α), f aμ) * r
theorem MeasureTheory.lintegral_lintegral_mul {α : Type u_1} {m : } {μ : } {β : Type u_5} [] {ν : } {f : αENNReal} {g : βENNReal} (hf : ) (hg : ) :
∫⁻ (x : α), ∫⁻ (y : β), f x * g yνμ = (∫⁻ (x : α), f xμ) * ∫⁻ (y : β), g yν
theorem MeasureTheory.lintegral_rw₁ {α : Type u_1} {β : Type u_2} {m : } {μ : } {f : αβ} {f' : αβ} (h : ) (g : βENNReal) :
∫⁻ (a : α), g (f a)μ = ∫⁻ (a : α), g (f' a)μ
theorem MeasureTheory.lintegral_rw₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : } {μ : } {f₁ : αβ} {f₁' : αβ} {f₂ : αγ} {f₂' : αγ} (h₁ : f₁ =ᶠ[] f₁') (h₂ : f₂ =ᶠ[] f₂') (g : βγENNReal) :
∫⁻ (a : α), g (f₁ a) (f₂ a)μ = ∫⁻ (a : α), g (f₁' a) (f₂' a)μ
@[simp]
theorem MeasureTheory.lintegral_indicator {α : Type u_1} {m : } {μ : } (f : αENNReal) {s : Set α} (hs : ) :
∫⁻ (a : α), μ = ∫⁻ (a : α) in s, f aμ
theorem MeasureTheory.lintegral_indicator₀ {α : Type u_1} {m : } {μ : } (f : αENNReal) {s : Set α} (hs : ) :
∫⁻ (a : α), μ = ∫⁻ (a : α) in s, f aμ
theorem MeasureTheory.lintegral_indicator_const₀ {α : Type u_1} {m : } {μ : } {s : Set α} (hs : ) (c : ENNReal) :
∫⁻ (a : α), Set.indicator s (fun x => c) aμ = c * μ s
theorem MeasureTheory.lintegral_indicator_const {α : Type u_1} {m : } {μ : } {s : Set α} (hs : ) (c : ENNReal) :
∫⁻ (a : α), Set.indicator s (fun x => c) aμ = c * μ s
theorem MeasureTheory.set_lintegral_eq_const {α : Type u_1} {m : } {μ : } {f : αENNReal} (hf : ) (r : ENNReal) :
∫⁻ (x : α) in {x | f x = r}, f xμ = r * μ {x | f x = r}
@[simp]
theorem MeasureTheory.lintegral_indicator_one {α : Type u_1} {m : } {μ : } {s : Set α} (hs : ) :
∫⁻ (a : α), μ = μ s
theorem MeasureTheory.lintegral_add_mul_meas_add_le_le_lintegral {α : Type u_1} {m : } {μ : } {f : αENNReal} {g : αENNReal} (hle : ) (hg : ) (ε : ENNReal) :
∫⁻ (a : α), f aμ + ε * μ {x | f x + ε g x} ∫⁻ (a : α), g aμ

A version of Markov's inequality for two functions. It doesn't follow from the standard Markov's inequality because we only assume measurability of g, not f.

theorem MeasureTheory.mul_meas_ge_le_lintegral₀ {α : Type u_1} {m : } {μ : } {f : αENNReal} (hf : ) (ε : ENNReal) :
ε * μ {x | ε f x} ∫⁻ (a : α), f aμ

Markov's inequality also known as Chebyshev's first inequality.

theorem MeasureTheory.mul_meas_ge_le_lintegral {α : Type u_1} {m : } {μ : } {f : αENNReal} (hf : ) (ε : ENNReal) :
ε * μ {x | ε f x} ∫⁻ (a : α), f aμ

Markov's inequality also known as Chebyshev's first inequality. For a version assuming AEMeasurable, see mul_meas_ge_le_lintegral₀.

theorem MeasureTheory.lintegral_eq_top_of_measure_eq_top_ne_zero {α : Type u_1} {m : } {μ : } {f : αENNReal} (hf : ) (hμf : μ {x | f x = } 0) :
∫⁻ (x : α), f xμ =
theorem MeasureTheory.setLintegral_eq_top_of_measure_eq_top_ne_zero {α : Type u_1} {m : } {μ : } {f : αENNReal} {s : Set α} (hf : ) (hμf : μ {x | x s f x = } 0) :
∫⁻ (x : α) in s, f xμ =
theorem MeasureTheory.measure_eq_top_of_lintegral_ne_top {α : Type u_1} {m : } {μ : } {f : αENNReal} (hf : ) (hμf : ∫⁻ (x : α), f xμ ) :
μ {x | f x = } = 0
theorem MeasureTheory.measure_eq_top_of_setLintegral_ne_top {α : Type u_1} {m : } {μ : } {f : αENNReal} {s : Set α} (hf : ) (hμf : ∫⁻ (x : α) in s, f xμ ) :
μ {x | x s f x = } = 0
theorem MeasureTheory.meas_ge_le_lintegral_div {α : Type u_1} {m : } {μ : } {f : αENNReal} (hf : ) {ε : ENNReal} (hε : ε 0) (hε' : ε ) :
μ {x | ε f x} (∫⁻ (a : α), f aμ) / ε

Markov's inequality also known as Chebyshev's first inequality.

theorem MeasureTheory.ae_eq_of_ae_le_of_lintegral_le {α : Type u_1} {m : } {μ : } {f : αENNReal} {g : αENNReal} (hfg : ) (hf : ∫⁻ (x : α), f xμ ) (hg : ) (hgf : ∫⁻ (x : α), g xμ ∫⁻ (x : α), f xμ) :
@[simp]
theorem MeasureTheory.lintegral_eq_zero_iff' {α : Type u_1} {m : } {μ : } {f : αENNReal} (hf : ) :
∫⁻ (a : α), f aμ = 0
@[simp]
theorem MeasureTheory.lintegral_eq_zero_iff {α : Type u_1} {m : } {μ : } {f : αENNReal} (hf : ) :
∫⁻ (a : α), f aμ = 0
theorem MeasureTheory.lintegral_pos_iff_support {α : Type u_1} {m : } {μ : } {f : αENNReal} (hf : ) :
0 < ∫⁻ (a : α), f aμ 0 < μ ()
theorem MeasureTheory.lintegral_iSup_ae {α : Type u_1} {m : } {μ : } {f : αENNReal} (hf : ∀ (n : ), Measurable (f n)) (h_mono : ∀ (n : ), ∀ᵐ (a : α) ∂μ, f n a f () a) :
∫⁻ (a : α), ⨆ (n : ), f n aμ = ⨆ (n : ), ∫⁻ (a : α), f n aμ

Weaker version of the monotone convergence theorem

theorem MeasureTheory.lintegral_sub' {α : Type u_1} {m : } {μ : } {f : αENNReal} {g : αENNReal} (hg : ) (hg_fin : ∫⁻ (a : α), g aμ ) (h_le : ) :
∫⁻ (a : α), f a - g aμ = ∫⁻ (a : α), f aμ - ∫⁻ (a : α), g aμ
theorem MeasureTheory.lintegral_sub {α : Type u_1} {m : } {μ : } {f : αENNReal} {g : αENNReal} (hg : ) (hg_fin : ∫⁻ (a : α), g aμ ) (h_le : ) :
∫⁻ (a : α), f a - g aμ = ∫⁻ (a : α), f aμ - ∫⁻ (a : α), g aμ
theorem MeasureTheory.lintegral_sub_le' {α : Type u_1} {m : } {μ : } (f : αENNReal) (g : αENNReal) (hf : ) :
∫⁻ (x : α), g xμ - ∫⁻ (x : α), f xμ ∫⁻ (x : α), g x - f xμ
theorem MeasureTheory.lintegral_sub_le {α : Type u_1} {m : } {μ : } (f : αENNReal) (g : αENNReal) (hf : ) :
∫⁻ (x : α), g xμ - ∫⁻ (x : α), f xμ ∫⁻ (x : α), g x - f xμ
theorem MeasureTheory.lintegral_strict_mono_of_ae_le_of_frequently_ae_lt {α : Type u_1} {m : } {μ : } {f : αENNReal} {g : αENNReal} (hg : ) (hfi : ∫⁻ (x : α), f xμ ) (h_le : ) (h : ∃ᵐ (x : α) ∂μ, f x g x) :
∫⁻ (x : α), f xμ < ∫⁻ (x : α), g xμ
theorem MeasureTheory.lintegral_strict_mono_of_ae_le_of_ae_lt_on {α : Type u_1} {m : } {μ : } {f : αENNReal} {g : αENNReal} (hg : ) (hfi : ∫⁻ (x : α), f xμ ) (h_le : ) {s : Set α} (hμs : μ s 0) (h : ∀ᵐ (x : α) ∂μ, x sf x < g x) :
∫⁻ (x : α), f xμ < ∫⁻ (x : α), g xμ
theorem MeasureTheory.lintegral_strict_mono {α : Type u_1} {m : } {μ : } {f : αENNReal} {g : αENNReal} (hμ : μ 0) (hg : ) (hfi : ∫⁻ (x : α), f xμ ) (h : ∀ᵐ (x : α) ∂μ, f x < g x) :
∫⁻ (x : α), f xμ < ∫⁻ (x : α), g xμ
theorem MeasureTheory.set_lintegral_strict_mono {α : Type u_1} {m : } {μ : } {f : αENNReal} {g : αENNReal} {s : Set α} (hsm : ) (hs : μ s 0) (hg : ) (hfi : ∫⁻ (x : α) in s, f xμ ) (h : ∀ᵐ (x : α) ∂μ, x sf x < g x) :
∫⁻ (x : α) in s, f xμ < ∫⁻ (x : α) in s, g xμ
theorem MeasureTheory.lintegral_iInf_ae {α : Type u_1} {m : } {μ : } {f : αENNReal} (h_meas : ∀ (n : ), Measurable (f n)) (h_mono : ∀ (n : ), f () ≤ᶠ[] 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} {m : } {μ : } {f : αENNReal} (h_meas : ∀ (n : ), Measurable (f n)) (h_anti : ) (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_liminf_le' {α : Type u_1} {m : } {μ : } {f : αENNReal} (h_meas : ∀ (n : ), AEMeasurable (f n)) :
∫⁻ (a : α), Filter.liminf (fun n => f n a) Filter.atTopμ Filter.liminf (fun n => ∫⁻ (a : α), f n aμ) Filter.atTop

Known as Fatou's lemma, version with AEMeasurable functions

theorem MeasureTheory.lintegral_liminf_le {α : Type u_1} {m : } {μ : } {f : αENNReal} (h_meas : ∀ (n : ), Measurable (f n)) :
∫⁻ (a : α), Filter.liminf (fun n => f n a) Filter.atTopμ Filter.liminf (fun n => ∫⁻ (a : α), f n aμ) Filter.atTop

Known as Fatou's lemma

theorem MeasureTheory.limsup_lintegral_le {α : Type u_1} {m : } {μ : } {f : αENNReal} {g : αENNReal} (hf_meas : ∀ (n : ), Measurable (f n)) (h_bound : ∀ (n : ), ) (h_fin : ∫⁻ (a : α), g aμ ) :
Filter.limsup (fun n => ∫⁻ (a : α), f n aμ) Filter.atTop ∫⁻ (a : α), Filter.limsup (fun n => f n a) Filter.atTopμ
theorem MeasureTheory.tendsto_lintegral_of_dominated_convergence {α : Type u_1} {m : } {μ : } {F : αENNReal} {f : αENNReal} (bound : αENNReal) (hF_meas : ∀ (n : ), Measurable (F n)) (h_bound : ∀ (n : ), F n ≤ᶠ[] bound) (h_fin : ∫⁻ (a : α), bound aμ ) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) :
Filter.Tendsto (fun n => ∫⁻ (a : α), F n aμ) Filter.atTop (nhds (∫⁻ (a : α), f aμ))

Dominated convergence theorem for nonnegative functions

theorem MeasureTheory.tendsto_lintegral_of_dominated_convergence' {α : Type u_1} {m : } {μ : } {F : αENNReal} {f : αENNReal} (bound : αENNReal) (hF_meas : ∀ (n : ), AEMeasurable (F n)) (h_bound : ∀ (n : ), F n ≤ᶠ[] bound) (h_fin : ∫⁻ (a : α), bound aμ ) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) :
Filter.Tendsto (fun n => ∫⁻ (a : α), F n aμ) Filter.atTop (nhds (∫⁻ (a : α), f aμ))

Dominated convergence theorem for nonnegative functions which are just almost everywhere measurable.

theorem MeasureTheory.tendsto_lintegral_filter_of_dominated_convergence {α : Type u_1} {m : } {μ : } {ι : Type u_5} {l : } {F : ιαENNReal} {f : αENNReal} (bound : αENNReal) (hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)) (h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a bound a) (h_fin : ∫⁻ (a : α), bound aμ ) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) l (nhds (f a))) :
Filter.Tendsto (fun n => ∫⁻ (a : α), F n aμ) l (nhds (∫⁻ (a : α), f aμ))

Dominated convergence theorem for filters with a countable basis

theorem MeasureTheory.lintegral_iSup_directed_of_measurable {α : Type u_1} {β : Type u_2} {m : } {μ : } [] {f : βαENNReal} (hf : ∀ (b : β), Measurable (f b)) (h_directed : Directed (fun x x_1 => x x_1) f) :
∫⁻ (a : α), ⨆ (b : β), f b aμ = ⨆ (b : β), ∫⁻ (a : α), f b aμ

Monotone convergence for a supremum over a directed family and indexed by a countable type

theorem MeasureTheory.lintegral_iSup_directed {α : Type u_1} {β : Type u_2} {m : } {μ : } [] {f : βαENNReal} (hf : ∀ (b : β), AEMeasurable (f b)) (h_directed : Directed (fun x x_1 => x x_1) f) :
∫⁻ (a : α), ⨆ (b : β), f b aμ = ⨆ (b : β), ∫⁻ (a : α), f b aμ

Monotone convergence for a supremum over a directed family and indexed by a countable type.

theorem MeasureTheory.lintegral_tsum {α : Type u_1} {β : Type u_2} {m : } {μ : } [] {f : βαENNReal} (hf : ∀ (i : β), AEMeasurable (f i)) :
∫⁻ (a : α), ∑' (i : β), f i aμ = ∑' (i : β), ∫⁻ (a : α), f i aμ
theorem MeasureTheory.lintegral_iUnion₀ {α : Type u_1} {β : Type u_2} {m : } {μ : } [] {s : βSet α} (hm : ∀ (i : β), ) (hd : ) (f : αENNReal) :
∫⁻ (a : α) in ⋃ (i : β), s i, f aμ = ∑' (i : β), ∫⁻ (a : α) in s i, f aμ
theorem MeasureTheory.lintegral_iUnion {α : Type u_1} {β : Type u_2} {m : } {μ : } [] {s : βSet α} (hm : ∀ (i : β), MeasurableSet (s i)) (hd : Pairwise (Disjoint on s)) (f : αENNReal) :
∫⁻ (a : α) in ⋃ (i : β), s i, f aμ = ∑' (i : β), ∫⁻ (a : α) in s i, f aμ
theorem MeasureTheory.lintegral_biUnion₀ {α : Type u_1} {β : Type u_2} {m : } {μ : } {t : Set β} {s : βSet α} (ht : ) (hm : ∀ (i : β), i t) (hd : ) (f : αENNReal) :
∫⁻ (a : α) in ⋃ (i : β) (_ : i t), s i, f aμ = ∑' (i : t), ∫⁻ (a : α) in s i, f aμ
theorem MeasureTheory.lintegral_biUnion {α : Type u_1} {β : Type u_2} {m : } {μ : } {t : Set β} {s : βSet α} (ht : ) (hm : ∀ (i : β), i tMeasurableSet (s i)) (hd : ) (f : αENNReal) :
∫⁻ (a : α) in ⋃ (i : β) (_ : i t), s i, f aμ = ∑' (i : t), ∫⁻ (a : α) in s i, f aμ
theorem MeasureTheory.lintegral_biUnion_finset₀ {α : Type u_1} {β : Type u_2} {m : } {μ : } {s : } {t : βSet α} (hd : Set.Pairwise (s) ()) (hm : ∀ (b : β), b s) (f : αENNReal) :
∫⁻ (a : α) in ⋃ (b : β) (_ : b s), t b, f aμ = Finset.sum s fun b => ∫⁻ (a : α) in t b, f aμ
theorem MeasureTheory.lintegral_biUnion_finset {α : Type u_1} {β : Type u_2} {m : } {μ : } {s : } {t : βSet α} (hd : Set.PairwiseDisjoint (s) t) (hm : ∀ (b : β), b sMeasurableSet (t b)) (f : αENNReal) :
∫⁻ (a : α) in ⋃ (b : β) (_ : b s), t b, f aμ = Finset.sum s fun b => ∫⁻ (a : α) in t b, f aμ
theorem MeasureTheory.lintegral_iUnion_le {α : Type u_1} {β : Type u_2} {m : } {μ : } [] (s : βSet α) (f : αENNReal) :
∫⁻ (a : α) in ⋃ (i : β), s i, f aμ ∑' (i : β), ∫⁻ (a : α) in s i, f aμ
theorem MeasureTheory.lintegral_union {α : Type u_1} {m : } {μ : } {f : αENNReal} {A : Set α} {B : Set α} (hB : ) (hAB : Disjoint A B) :
∫⁻ (a : α) in A B, f aμ = ∫⁻ (a : α) in A, f aμ + ∫⁻ (a : α) in B, f aμ
theorem MeasureTheory.lintegral_union_le {α : Type u_1} {m : } {μ : } (f : αENNReal) (s : Set α) (t : Set α) :
∫⁻ (a : α) in s t, f aμ ∫⁻ (a : α) in s, f aμ + ∫⁻ (a : α) in t, f aμ
theorem MeasureTheory.lintegral_inter_add_diff {α : Type u_1} {m : } {μ : } {B : Set α} (f : αENNReal) (A : Set α) (hB : ) :
∫⁻ (x : α) in A B, f xμ + ∫⁻ (x : α) in A \ B, f xμ = ∫⁻ (x : α) in A, f xμ
theorem MeasureTheory.lintegral_add_compl {α : Type u_1} {m : } {μ : } (f : αENNReal) {A : Set α} (hA : ) :
∫⁻ (x : α) in A, f xμ + ∫⁻ (x : α) in A, f xμ = ∫⁻ (x : α), f xμ
theorem MeasureTheory.lintegral_max {α : Type u_1} {m : } {μ : } {f : αENNReal} {g : αENNReal} (hf : ) (hg : ) :
∫⁻ (x : α), max (f x) (g x)μ = ∫⁻ (x : α) in {x | f x g x}, g xμ + ∫⁻ (x : α) in {x | g x < f x}, f xμ
theorem MeasureTheory.set_lintegral_max {α : Type u_1} {m : } {μ : } {f : αENNReal} {g : αENNReal} (hf : ) (hg : ) (s : Set α) :
∫⁻ (x : α) in s, max (f x) (g x)μ = ∫⁻ (x : α) in s {x | f x g x}, g xμ + ∫⁻ (x : α) in s {x | g x < f x}, f xμ
theorem MeasureTheory.lintegral_map {α : Type u_1} {β : Type u_2} {m : } {μ : } {mβ : } {f : βENNReal} {g : αβ} (hf : ) (hg : ) :
∫⁻ (a : β), f a = ∫⁻ (a : α), f (g a)μ
theorem MeasureTheory.lintegral_map' {α : Type u_1} {β : Type u_2} {m : } {μ : } {mβ : } {f : βENNReal} {g : αβ} (hf : ) (hg : ) :
∫⁻ (a : β), f a = ∫⁻ (a : α), f (g a)μ
theorem MeasureTheory.lintegral_map_le {α : Type u_1} {β : Type u_2} {m : } {μ : } {mβ : } (f : βENNReal) {g : αβ} (hg : ) :
∫⁻ (a : β), f a ∫⁻ (a : α), f (g a)μ
theorem MeasureTheory.lintegral_comp {α : Type u_1} {β : Type u_2} {m : } {μ : } [] {f : βENNReal} {g : αβ} (hf : ) (hg : ) :
MeasureTheory.lintegral μ (f g) = ∫⁻ (a : β), f a
theorem MeasureTheory.set_lintegral_map {α : Type u_1} {β : Type u_2} {m : } {μ : } [] {f : βENNReal} {g : αβ} {s : Set β} (hs : ) (hf : ) (hg : ) :
∫⁻ (y : β) in s, f y = ∫⁻ (x : α) in g ⁻¹' s, f (g x)μ
theorem MeasureTheory.lintegral_indicator_const_comp {α : Type u_1} {β : Type u_2} {m : } {μ : } {mβ : } {f : αβ} {s : Set β} (hf : ) (hs : ) (c : ENNReal) :
∫⁻ (a : α), Set.indicator s (fun x => c) (f a)μ = c * μ (f ⁻¹' s)
theorem MeasurableEmbedding.lintegral_map {α : Type u_1} {β : Type u_2} {m : } {μ : } [] {g : αβ} (hg : ) (f : βENNReal) :
∫⁻ (a : β), f a = ∫⁻ (a : α), f (g a)μ

If g : α → β is a measurable embedding and f : β → ℝ≥0∞ is any function (not necessarily measurable), then ∫⁻ a, f a ∂(map g μ) = ∫⁻ a, f (g a) ∂μ. Compare with lintegral_map which applies to any measurable g : α → β but requires that f is measurable as well.

theorem MeasureTheory.lintegral_map_equiv {α : Type u_1} {β : Type u_2} {m : } {μ : } [] (f : βENNReal) (g : α ≃ᵐ β) :
∫⁻ (a : β), f a = ∫⁻ (a : α), f (g a)μ

The lintegral transforms appropriately under a measurable equivalence g : α ≃ᵐ β. (Compare lintegral_map, which applies to a wider class of functions g : α → β, but requires measurability of the function being integrated.)

theorem MeasureTheory.MeasurePreserving.lintegral_comp {α : Type u_1} {β : Type u_2} {m : } {μ : } {mb : } {ν : } {g : αβ} (hg : ) {f : βENNReal} (hf : ) :
∫⁻ (a : α), f (g a)μ = ∫⁻ (b : β), f bν
theorem MeasureTheory.MeasurePreserving.lintegral_comp_emb {α : Type u_1} {β : Type u_2} {m : } {μ : } {mb : } {ν : } {g : αβ} (hg : ) (hge : ) (f : βENNReal) :
∫⁻ (a : α), f (g a)μ = ∫⁻ (b : β), f bν
theorem MeasureTheory.MeasurePreserving.set_lintegral_comp_preimage {α : Type u_1} {β : Type u_2} {m : } {μ : } {mb : } {ν : } {g : αβ} (hg : ) {s : Set β} (hs : ) {f : βENNReal} (hf : ) :
∫⁻ (a : α) in g ⁻¹' s, f (g a)μ = ∫⁻ (b : β) in s, f bν
theorem MeasureTheory.MeasurePreserving.set_lintegral_comp_preimage_emb {α : Type u_1} {β : Type u_2} {m : } {μ : } {mb : } {ν : } {g : αβ} (hg : ) (hge : ) (f : βENNReal) (s : Set β) :
∫⁻ (a : α) in g ⁻¹' s, f (g a)μ = ∫⁻ (b : β) in s, f bν
theorem MeasureTheory.MeasurePreserving.set_lintegral_comp_emb {α : Type u_1} {β : Type u_2} {m : } {μ : } {mb : } {ν : } {g : αβ} (hg : ) (hge : ) (f : βENNReal) (s : Set α) :
∫⁻ (a : α) in s, f (g a)μ = ∫⁻ (b : β) in g '' s, f bν
theorem MeasureTheory.lintegral_dirac' {α : Type u_1} [] (a : α) {f : αENNReal} (hf : ) :
∫⁻ (a : α), f a = f a
theorem MeasureTheory.lintegral_dirac {α : Type u_1} [] (a : α) (f : αENNReal) :
∫⁻ (a : α), f a = f a
theorem MeasureTheory.set_lintegral_dirac' {α : Type u_1} [] {a : α} {f : αENNReal} (hf : ) {s : Set α} (hs : ) [Decidable (a s)] :
∫⁻ (x : α) in s, f x = if a s then f a else 0
theorem MeasureTheory.set_lintegral_dirac {α : Type u_1} [] {a : α} (f : αENNReal) (s : Set α) [Decidable (a s)] :
∫⁻ (x : α) in s, f x = if a s then f a else 0
theorem MeasureTheory.lintegral_count' {α : Type u_1} [] {f : αENNReal} (hf : ) :
∫⁻ (a : α), f aMeasureTheory.Measure.count = ∑' (a : α), f a
theorem MeasureTheory.lintegral_count {α : Type u_1} [] (f : αENNReal) :
∫⁻ (a : α), f aMeasureTheory.Measure.count = ∑' (a : α), f a
theorem ENNReal.tsum_const_eq {α : Type u_1} [] (c : ENNReal) :
∑' (x : α), c = c * MeasureTheory.Measure.count Set.univ
theorem ENNReal.count_const_le_le_of_tsum_le {α : Type u_1} [] {a : αENNReal} (a_mble : ) {c : ENNReal} (tsum_le_c : ∑' (i : α), a i c) {ε : ENNReal} (ε_ne_zero : ε 0) (ε_ne_top : ε ) :
MeasureTheory.Measure.count {i | ε a i} c / ε

Markov's inequality for the counting measure with hypothesis using tsum in ℝ≥0∞.

theorem NNReal.count_const_le_le_of_tsum_le {α : Type u_1} [] {a : αNNReal} (a_mble : ) (a_summable : ) {c : NNReal} (tsum_le_c : ∑' (i : α), a i c) {ε : NNReal} (ε_ne_zero : ε 0) :
MeasureTheory.Measure.count {i | ε a i} c / ε

Markov's inequality for counting measure with hypothesis using tsum in ℝ≥0.

### Lebesgue integral over finite and countable types and sets #

theorem MeasureTheory.lintegral_countable' {α : Type u_1} {m : } {μ : } [] (f : αENNReal) :
∫⁻ (a : α), f aμ = ∑' (a : α), f a * μ {a}
theorem MeasureTheory.lintegral_singleton' {α : Type u_1} {m : } {μ : } {f : αENNReal} (hf : ) (a : α) :
∫⁻ (x : α) in {a}, f xμ = f a * μ {a}
theorem MeasureTheory.lintegral_singleton {α : Type u_1} {m : } {μ : } (f : αENNReal) (a : α) :
∫⁻ (x : α) in {a}, f xμ = f a * μ {a}
theorem MeasureTheory.lintegral_countable {α : Type u_1} {m : } {μ : } (f : αENNReal) {s : Set α} (hs : ) :
∫⁻ (a : α) in s, f aμ = ∑' (a : s), f a * μ {a}
theorem MeasureTheory.lintegral_insert {α : Type u_1} {m : } {μ : } {a : α} {s : Set α} (h : ¬a s) (f : αENNReal) :
∫⁻ (x : α) in insert a s, f xμ = f a * μ {a} + ∫⁻ (x : α) in s, f xμ
theorem MeasureTheory.lintegral_finset {α : Type u_1} {m : } {μ : } (s : ) (f : αENNReal) :
∫⁻ (x : α) in s, f xμ = Finset.sum s fun x => f x * μ {x}
theorem MeasureTheory.lintegral_fintype {α : Type u_1} {m : } {μ : } [] (f : αENNReal) :
∫⁻ (x : α), f xμ = Finset.sum Finset.univ fun x => f x * μ {x}
theorem MeasureTheory.lintegral_unique {α : Type u_1} {m : } {μ : } [] (f : αENNReal) :
∫⁻ (x : α), f xμ = f default * μ Set.univ
theorem MeasureTheory.ae_lt_top {α : Type u_1} {m : } {μ : } {f : αENNReal} (hf : ) (h2f : ∫⁻ (x : α), f xμ ) :
∀ᵐ (x : α) ∂μ, f x <
theorem MeasureTheory.ae_lt_top' {α : Type u_1} {m : } {μ : } {f : αENNReal} (hf : ) (h2f : ∫⁻ (x : α), f xμ ) :
∀ᵐ (x : α) ∂μ, f x <
theorem MeasureTheory.set_lintegral_lt_top_of_bddAbove {α : Type u_1} {m : } {μ : } {s : Set α} (hs : μ s ) {f : αNNReal} (hf : ) (hbdd : BddAbove (f '' s)) :
∫⁻ (x : α) in s, ↑(f x)μ <
theorem MeasureTheory.set_lintegral_lt_top_of_isCompact {α : Type u_1} {m : } {μ : } [] {s : Set α} (hs : μ s ) (hsc : ) {f : αNNReal} (hf : ) :
∫⁻ (x : α) in s, ↑(f x)μ <
theorem IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal {α : Type u_5} [] (μ : ) [μ_fin : ] {f : αENNReal} (f_bdd : c, ∀ (x : α), f x c) :
∫⁻ (x : α), f xμ <
def MeasureTheory.Measure.withDensity {α : Type u_1} {m : } (μ : ) (f : αENNReal) :

Given a measure μ : Measure α and a function f : α → ℝ≥0∞, μ.withDensity f is the measure such that for a measurable set s we have μ.withDensity f s = ∫⁻ a in s, f a ∂μ.

Instances For
@[simp]
theorem MeasureTheory.withDensity_apply {α : Type u_1} {m : } {μ : } (f : αENNReal) {s : Set α} (hs : ) :
s = ∫⁻ (a : α) in s, f aμ
theorem MeasureTheory.withDensity_congr_ae {α : Type u_1} {m : } {μ : } {f : αENNReal} {g : αENNReal} (h : ) :
theorem MeasureTheory.withDensity_add_left {α : Type u_1} {m : } {μ : } {f : αENNReal} (hf : ) (g : αENNReal) :
theorem MeasureTheory.withDensity_add_right {α : Type u_1} {m : } {μ : } (f : αENNReal) {g : αENNReal} (hg : ) :
theorem MeasureTheory.withDensity_add_measure {α : Type u_1} {m : } (μ : ) (ν : ) (f : αENNReal) :
theorem MeasureTheory.withDensity_sum {α : Type u_1} {ι : Type u_5} {m : } (μ : ) (f : αENNReal) :
theorem MeasureTheory.withDensity_smul {α : Type u_1} {m : } {μ : } (r : ENNReal) {f : αENNReal} (hf : ) :
theorem MeasureTheory.withDensity_smul' {α : Type u_1} {m : } {μ : } (r : ENNReal) (f : αENNReal) (hr : r ) :
theorem MeasureTheory.isFiniteMeasure_withDensity {α : Type u_1} {m : } {μ : } {f : αENNReal} (hf : ∫⁻ (a : α), f aμ ) :
theorem MeasureTheory.withDensity_absolutelyContinuous {α : Type u_1} {m : } (μ : ) (f : αENNReal) :
@[simp]
theorem MeasureTheory.withDensity_zero {α : Type u_1} {m : } {μ : } :
@[simp]
theorem MeasureTheory.withDensity_one {α : Type u_1} {m : } {μ : } :
theorem MeasureTheory.withDensity_tsum {α : Type u_1} {m : } {μ : } {f : αENNReal} (h : ∀ (i : ), Measurable (f i)) :
theorem MeasureTheory.withDensity_indicator {α : Type u_1} {m : } {μ : } {s : Set α} (hs : ) (f : αENNReal) :
theorem MeasureTheory.withDensity_indicator_one {α : Type u_1} {m : } {μ : } {s : Set α} (hs : ) :
theorem MeasureTheory.restrict_withDensity {α : Type u_1} {m : } {μ : } {s : Set α} (hs : ) (f : αENNReal) :
theorem MeasureTheory.withDensity_eq_zero {α : Type u_1} {m : } {μ : } {f : αENNReal} (hf : ) (h : ) :
theorem MeasureTheory.withDensity_apply_eq_zero {α : Type u_1} {m : } {μ : } {f : αENNReal} {s : Set α} (hf : ) :
s = 0 μ ({x | f x 0} s) = 0
theorem MeasureTheory.ae_withDensity_iff {α : Type u_1} {m : } {μ : } {p : αProp} {f : αENNReal} (hf : ) :
(∀ᵐ (x : α) ∂, p x) ∀ᵐ (x : α) ∂μ, f x 0p x
theorem MeasureTheory.ae_withDensity_iff_ae_restrict {α : Type u_1} {m : } {μ : } {p : αProp} {f : αENNReal} (hf : ) :
(∀ᵐ (x : α) ∂, p x) ∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ {x | f x 0}, p x
theorem MeasureTheory.aemeasurable_withDensity_ennreal_iff {α : Type u_1} {m : } {μ : } {f : αNNReal} (hf : ) {g : αENNReal} :
AEMeasurable fun x => ↑(f x) * g x
theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul {α : Type u_1} {m0 : } (μ : ) {f : αENNReal} (h_mf : ) {g : αENNReal} :
∫⁻ (a : α), g a = ∫⁻ (a : α), (f * g) aμ

This is Exercise 1.2.1 from [tao2010]. It allows you to express integration of a measurable function with respect to (μ.withDensity f) as an integral with respect to μ, called the base measure. μ is often the Lebesgue measure, and in this circumstance f is the probability density function, and (μ.withDensity f) represents any continuous random variable as a probability measure, such as the uniform distribution between 0 and 1, the Gaussian distribution, the exponential distribution, the Beta distribution, or the Cauchy distribution (see Section 2.4 of [wasserman2004]). Thus, this method shows how to one can calculate expectations, variances, and other moments as a function of the probability density function.

theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul {α : Type u_1} {m0 : } (μ : ) {f : αENNReal} {g : αENNReal} (hf : ) (hg : ) {s : Set α} (hs : ) :
∫⁻ (x : α) in s, g x = ∫⁻ (x : α) in s, (f * g) xμ
theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀' {α : Type u_1} {m0 : } {μ : } {f : αENNReal} (hf : ) {g : αENNReal} (hg : ) :
∫⁻ (a : α), g a = ∫⁻ (a : α), (f * g) aμ

The Lebesgue integral of g with respect to the measure μ.withDensity f coincides with the integral of f * g. This version assumes that g is almost everywhere measurable. For a version without conditions on g but requiring that f is almost everywhere finite, see lintegral_withDensity_eq_lintegral_mul_non_measurable

theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀ {α : Type u_1} {m0 : } {μ : } {f : αENNReal} (hf : ) {g : αENNReal} (hg : ) :
∫⁻ (a : α), g a = ∫⁻ (a : α), (f * g) aμ
theorem MeasureTheory.lintegral_withDensity_le_lintegral_mul {α : Type u_1} {m0 : } (μ : ) {f : αENNReal} (f_meas : ) (g : αENNReal) :
∫⁻ (a : α), g a ∫⁻ (a : α), (f * g) aμ
theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable {α : Type u_1} {m0 : } (μ : ) {f : αENNReal} (f_meas : ) (hf : ∀ᵐ (x : α) ∂μ, f x < ) (g : αENNReal) :
∫⁻ (a : α), g a = ∫⁻ (a : α), (f * g) aμ
theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable {α : Type u_1} {m0 : } (μ : ) {f : αENNReal} (f_meas : ) (g : αENNReal) {s : Set α} (hs : ) (hf : ∀ᵐ (x : α) ∂, f x < ) :
∫⁻ (a : α) in s, g a = ∫⁻ (a : α) in s, (f * g) aμ
theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable₀ {α : Type u_1} {m0 : } (μ : ) {f : αENNReal} (hf : ) (h'f : ∀ᵐ (x : α) ∂μ, f x < ) (g : αENNReal) :
∫⁻ (a : α), g a = ∫⁻ (a : α), (f * g) aμ
theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable₀ {α : Type u_1} {m0 : } (μ : ) {f : αENNReal} {s : Set α} (hf : ) (g : αENNReal) (hs : ) (h'f : ∀ᵐ (x : α) ∂, f x < ) :
∫⁻ (a : α) in s, g a = ∫⁻ (a : α) in s, (f * g) aμ
theorem MeasureTheory.withDensity_mul {α : Type u_1} {m0 : } (μ : ) {f : αENNReal} {g : αENNReal} (hf : ) (hg : ) :
theorem MeasureTheory.exists_pos_lintegral_lt_of_sigmaFinite {α : Type u_1} {m0 : } (μ : ) {ε : ENNReal} (ε0 : ε 0) :
g, (∀ (x : α), 0 < g x) ∫⁻ (x : α), ↑(g x)μ < ε

In a sigma-finite measure space, there exists an integrable function which is positive everywhere (and with an arbitrarily small integral).

theorem MeasureTheory.lintegral_trim {α : Type u_1} {m : } {m0 : } {μ : } (hm : m m0) {f : αENNReal} (hf : ) :
∫⁻ (a : α), f a = ∫⁻ (a : α), f aμ
theorem MeasureTheory.lintegral_trim_ae {α : Type u_1} {m : } {m0 : } {μ : } (hm : m m0) {f : αENNReal} (hf : ) :
∫⁻ (a : α), f a = ∫⁻ (a : α), f aμ
theorem MeasureTheory.univ_le_of_forall_fin_meas_le {α : Type u_1} {m : } {m0 : } {μ : } (hm : m m0) (C : ENNReal) {f : Set αENNReal} (hf : ∀ (s : Set α), μ s f s C) (h_F_lim : ∀ (S : Set α), (∀ (n : ), MeasurableSet (S n)) → f (⋃ (n : ), S n) ⨆ (n : ), f (S n)) :
f Set.univ C
theorem MeasureTheory.lintegral_le_of_forall_fin_meas_le_of_measurable {α : Type u_1} {m : } {m0 : } {μ : } (hm : m m0) (C : ENNReal) {f : αENNReal} (hf_meas : ) (hf : ∀ (s : Set α), μ s ∫⁻ (x : α) in s, f xμ C) :
∫⁻ (x : α), f xμ C

If the Lebesgue integral of a function is bounded by some constant on all sets with finite measure in a sub-σ-algebra and the measure is σ-finite on that sub-σ-algebra, then the integral over the whole space is bounded by that same constant. Version for a measurable function. See lintegral_le_of_forall_fin_meas_le' for the more general AEMeasurable version.

theorem MeasureTheory.lintegral_le_of_forall_fin_meas_le' {α : Type u_1} {m : } {m0 : } {μ : } (hm : m m0) (C : ENNReal) {f : αENNReal} (hf_meas : ) (hf : ∀ (s : Set α), μ s ∫⁻ (x : α) in s, f xμ C) :
∫⁻ (x : α), f xμ C

If the Lebesgue integral of a function is bounded by some constant on all sets with finite measure in a sub-σ-algebra and the measure is σ-finite on that sub-σ-algebra, then the integral over the whole space is bounded by that same constant.

theorem MeasureTheory.lintegral_le_of_forall_fin_meas_le {α : Type u_1} [] {μ : } (C : ENNReal) {f : αENNReal} (hf_meas : ) (hf : ∀ (s : Set α), μ s ∫⁻ (x : α) in s, f xμ C) :
∫⁻ (x : α), f xμ C

If the Lebesgue integral of a function is bounded by some constant on all sets with finite measure and the measure is σ-finite, then the integral over the whole space is bounded by that same constant.

theorem MeasureTheory.SimpleFunc.exists_lt_lintegral_simpleFunc_of_lt_lintegral {α : Type u_1} {m : } {μ : } {f : } {L : ENNReal} (hL : L < ∫⁻ (x : α), ↑(f x)μ) :
g, (∀ (x : α), g x f x) ∫⁻ (x : α), ↑(g x)μ < L < ∫⁻ (x : α), ↑(g x)μ
theorem MeasureTheory.exists_lt_lintegral_simpleFunc_of_lt_lintegral {α : Type u_1} {m : } {μ : } {f : αNNReal} {L : ENNReal} (hL : L < ∫⁻ (x : α), ↑(f x)μ) :
g, (∀ (x : α), g x f x) ∫⁻ (x : α), ↑(g x)μ < L < ∫⁻ (x : α), ↑(g x)μ

A sigma-finite measure is absolutely continuous with respect to some finite measure.

theorem MeasureTheory.tendsto_measure_of_ae_tendsto_indicator {α : Type u_5} [] {A : Set α} {ι : Type u_6} (L : ) {As : ιSet α} {μ : } (A_mble : ) (As_mble : ∀ (i : ι), MeasurableSet (As i)) {B : Set α} (B_mble : ) (B_finmeas : μ B ) (As_le_B : ∀ᶠ (i : ι) in L, As i B) (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun i => Set.indicator (As i) 1 x) L (nhds ())) :
Filter.Tendsto (fun i => μ (As i)) L (nhds (μ A))

If the indicators of measurable sets Aᵢ tend pointwise almost everywhere to the indicator of a measurable set A and we eventually have Aᵢ ⊆ B for some set B of finite measure, then the measures of Aᵢ tend to the measure of A.

theorem MeasureTheory.tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure {α : Type u_5} [] {A : Set α} {ι : Type u_6} (L : ) {As : ιSet α} {μ : } (A_mble : ) (As_mble : ∀ (i : ι), MeasurableSet (As i)) (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun i => Set.indicator (As i) 1 x) L (nhds ())) :
Filter.Tendsto (fun i => μ (As i)) L (nhds (μ A))

If μ is a finite measure and the indicators of measurable sets Aᵢ tend pointwise almost everywhere to the indicator of a measurable set A, then the measures μ Aᵢ tend to the measure μ A.