# mathlib3documentation

measure_theory.integral.lebesgue

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 measure_theory.restrict_dirac' {α : Type u_1} {mα : measurable_space α} {a : α} {s : set α} (hs : measurable_set s) [decidable (a s)] :
= ite (a s) 0
theorem measure_theory.restrict_dirac {α : Type u_1} {mα : measurable_space α} {a : α} {s : set α} [decidable (a s)] :
= ite (a s) 0
@[irreducible]
noncomputable def measure_theory.lintegral {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) (f : α ennreal) :

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

Equations

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.

theorem measure_theory.lintegral_mono' {α : Type u_1} {m : measurable_space α} ⦃μ ν : measure_theory.measure α⦄ (hμν : μ ν) ⦃f g : α ennreal (hfg : f g) :
∫⁻ (a : α), f a μ ∫⁻ (a : α), g a ν
theorem measure_theory.lintegral_mono {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} ⦃f g : α ennreal (hfg : f g) :
∫⁻ (a : α), f a μ ∫⁻ (a : α), g a μ
theorem measure_theory.lintegral_mono_nnreal {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α nnreal} (h : f g) :
∫⁻ (a : α), (f a) μ ∫⁻ (a : α), (g a) μ
theorem measure_theory.supr_lintegral_measurable_le_eq_lintegral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : α ennreal) :
( (g : α ennreal) (g_meas : (hg : g f), ∫⁻ (a : α), g a μ) = ∫⁻ (a : α), f a μ
theorem measure_theory.lintegral_mono_set {α : Type u_1} {m : measurable_space α} ⦃μ : measure_theory.measure α⦄ {s t : set α} {f : α ennreal} (hst : s t) :
∫⁻ (x : α) in s, f x μ ∫⁻ (x : α) in t, f x μ
theorem measure_theory.lintegral_mono_set' {α : Type u_1} {m : measurable_space α} ⦃μ : measure_theory.measure α⦄ {s t : set α} {f : α ennreal} (hst : s ≤ᵐ[μ] t) :
∫⁻ (x : α) in s, f x μ ∫⁻ (x : α) in t, f x μ
@[simp]
theorem measure_theory.lintegral_const {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (c : ennreal) :
∫⁻ (a : α), c μ = c *
theorem measure_theory.lintegral_zero {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} :
∫⁻ (a : α), 0 μ = 0
@[simp]
theorem measure_theory.lintegral_one {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} :
∫⁻ (a : α), 1 μ =
theorem measure_theory.set_lintegral_const {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (s : set α) (c : ennreal) :
∫⁻ (a : α) in s, c μ = c * μ s
theorem measure_theory.set_lintegral_one {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (s : set α) :
∫⁻ (a : α) in s, 1 μ = μ s
theorem measure_theory.set_lintegral_const_lt_top {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (s : set α) {c : ennreal} (hc : c ) :
∫⁻ (a : α) in s, c μ <
theorem measure_theory.lintegral_const_lt_top {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {c : ennreal} (hc : c ) :
∫⁻ (a : α), c μ <
theorem measure_theory.exists_measurable_le_lintegral_eq {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) (f : α ennreal) :
(g : α ennreal), 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 measure_theory.lintegral_eq_nnreal {α : Type u_1} {m : measurable_space α} (f : α ennreal) (μ : measure_theory.measure α) :
∫⁻ (a : α), f a μ = (φ : (hf : (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 measure_theory.exists_simple_func_forall_lintegral_sub_lt_of_pos {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (h : ∫⁻ (x : α), f x μ ) {ε : ennreal} (hε : ε 0) :
(φ : , ( (x : α), (φ x) f x) (ψ : , ( (x : α), (ψ x) f x) - φ)).lintegral μ < ε
theorem measure_theory.supr_lintegral_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {ι : Sort u_2} (f : ι ) :
( (i : ι), ∫⁻ (a : α), f i a μ) ∫⁻ (a : α), ( (i : ι), f i a) μ
theorem measure_theory.supr₂_lintegral_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {ι : Sort u_2} {ι' : ι Sort u_3} (f : Π (i : ι), ι' i ) :
( (i : ι) (j : ι' i), ∫⁻ (a : α), f i j a μ) ∫⁻ (a : α), ( (i : ι) (j : ι' i), f i j a) μ
theorem measure_theory.le_infi_lintegral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {ι : Sort u_2} (f : ι ) :
∫⁻ (a : α), ( (i : ι), f i a) μ (i : ι), ∫⁻ (a : α), f i a μ
theorem measure_theory.le_infi₂_lintegral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {ι : Sort u_2} {ι' : ι Sort u_3} (f : Π (i : ι), ι' i ) :
∫⁻ (a : α), ( (i : ι) (h : ι' i), f i h a) μ (i : ι) (h : ι' i), ∫⁻ (a : α), f i h a μ
theorem measure_theory.lintegral_mono_ae {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α ennreal} (h : ∀ᵐ (a : α) μ, f a g a) :
∫⁻ (a : α), f a μ ∫⁻ (a : α), g a μ
theorem measure_theory.set_lintegral_mono_ae {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {s : set α} {f g : α ennreal} (hf : measurable f) (hg : measurable g) (hfg : ∀ᵐ (x : α) μ, x s f x g x) :
∫⁻ (x : α) in s, f x μ ∫⁻ (x : α) in s, g x μ
theorem measure_theory.set_lintegral_mono {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {s : set α} {f g : α ennreal} (hf : measurable f) (hg : measurable g) (hfg : (x : α), x s f x g x) :
∫⁻ (x : α) in s, f x μ ∫⁻ (x : α) in s, g x μ
theorem measure_theory.lintegral_congr_ae {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α ennreal} (h : f =ᵐ[μ] g) :
∫⁻ (a : α), f a μ = ∫⁻ (a : α), g a μ
theorem measure_theory.lintegral_congr {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α ennreal} (h : (a : α), f a = g a) :
∫⁻ (a : α), f a μ = ∫⁻ (a : α), g a μ
theorem measure_theory.set_lintegral_congr {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} {s t : set α} (h : s =ᵐ[μ] t) :
∫⁻ (x : α) in s, f x μ = ∫⁻ (x : α) in t, f x μ
theorem measure_theory.set_lintegral_congr_fun {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α ennreal} {s : set α} (hs : measurable_set s) (hfg : ∀ᵐ (x : α) μ, x s f x = g x) :
∫⁻ (x : α) in s, f x μ = ∫⁻ (x : α) in s, g x μ
theorem measure_theory.lintegral_nnnorm_eq_of_ae_nonneg {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α } (h_nonneg : 0 ≤ᵐ[μ] f) :
∫⁻ (x : α), f x‖₊ μ = ∫⁻ (x : α), ennreal.of_real (f x) μ
theorem measure_theory.lintegral_nnnorm_eq_of_nonneg {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α } (h_nonneg : 0 f) :
∫⁻ (x : α), f x‖₊ μ = ∫⁻ (x : α), ennreal.of_real (f x) μ
theorem measure_theory.lintegral_supr {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : } (hf : (n : ), measurable (f n)) (h_mono : monotone f) :
∫⁻ (a : α), ( (n : ), f n a) μ = (n : ), ∫⁻ (a : α), f n a μ

Monotone convergence theorem -- sometimes called Beppo-Levi convergence.

See `lintegral_supr_directed` for a more general form.

theorem measure_theory.lintegral_supr' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : } (hf : (n : ), ae_measurable (f n) μ) (h_mono : ∀ᵐ (x : α) μ, monotone (λ (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 measure_theory.lintegral_tendsto_of_tendsto_of_monotone {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : } {F : α ennreal} (hf : (n : ), ae_measurable (f n) μ) (h_mono : ∀ᵐ (x : α) μ, monotone (λ (n : ), f n x)) (h_tendsto : ∀ᵐ (x : α) μ, filter.tendsto (λ (n : ), f n x) filter.at_top (nhds (F x))) :
filter.tendsto (λ (n : ), ∫⁻ (x : α), f n x μ) filter.at_top (nhds (∫⁻ (x : α), F x μ))

Monotone convergence theorem expressed with limits

theorem measure_theory.lintegral_eq_supr_eapprox_lintegral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (hf : measurable f) :
∫⁻ (a : α), f a μ = (n : ),
theorem measure_theory.exists_pos_set_lintegral_lt_of_measure_lt {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (h : ∫⁻ (x : α), f x μ ) {ε : ennreal} (hε : ε 0) :
(δ : ennreal) (H : δ > 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 measure_theory.tendsto_set_lintegral_zero {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {ι : Type u_2} {f : α ennreal} (h : ∫⁻ (x : α), f x μ ) {l : filter ι} {s : ι set α} (hl : filter.tendsto (μ s) l (nhds 0)) :
filter.tendsto (λ (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 measure_theory.le_lintegral_add {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f 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 measure_theory.lintegral_add_aux {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α ennreal} (hf : measurable f) (hg : measurable g) :
∫⁻ (a : α), f a + g a μ = ∫⁻ (a : α), f a μ + ∫⁻ (a : α), g a μ
@[simp]
theorem measure_theory.lintegral_add_left {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (hf : measurable f) (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 `measure_theory.lintegral_add_right` and primed versions of these lemmas.

theorem measure_theory.lintegral_add_left' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (hf : μ) (g : α ennreal) :
∫⁻ (a : α), f a + g a μ = ∫⁻ (a : α), f a μ + ∫⁻ (a : α), g a μ
theorem measure_theory.lintegral_add_right' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : α ennreal) {g : α ennreal} (hg : μ) :
∫⁻ (a : α), f a + g a μ = ∫⁻ (a : α), f a μ + ∫⁻ (a : α), g a μ
@[simp]
theorem measure_theory.lintegral_add_right {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : α ennreal) {g : α ennreal} (hg : measurable g) :
∫⁻ (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 `measure_theory.lintegral_add_left` and primed versions of these lemmas.

@[simp]
theorem measure_theory.lintegral_smul_measure {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (c : ennreal) (f : α ennreal) :
∫⁻ (a : α), f a c μ = c * ∫⁻ (a : α), f a μ
@[simp]
theorem measure_theory.lintegral_sum_measure {α : Type u_1} {m : measurable_space α} {ι : Type u_2} (f : α ennreal) (μ : ι ) :
∫⁻ (a : α), f a = ∑' (i : ι), ∫⁻ (a : α), f a μ i
theorem measure_theory.has_sum_lintegral_measure {α : Type u_1} {ι : Type u_2} {m : measurable_space α} (f : α ennreal) (μ : ι ) :
has_sum (λ (i : ι), ∫⁻ (a : α), f a μ i) (∫⁻ (a : α), f a
@[simp]
theorem measure_theory.lintegral_add_measure {α : Type u_1} {m : measurable_space α} (f : α ennreal) (μ ν : measure_theory.measure α) :
∫⁻ (a : α), f a + ν) = ∫⁻ (a : α), f a μ + ∫⁻ (a : α), f a ν
@[simp]
theorem measure_theory.lintegral_finset_sum_measure {α : Type u_1} {ι : Type u_2} {m : measurable_space α} (s : finset ι) (f : α ennreal) (μ : ι ) :
∫⁻ (a : α), f a s.sum (λ (i : ι), μ i) = s.sum (λ (i : ι), ∫⁻ (a : α), f a μ i)
@[simp]
theorem measure_theory.lintegral_zero_measure {α : Type u_1} {m : measurable_space α} (f : α ennreal) :
∫⁻ (a : α), f a 0 = 0
theorem measure_theory.set_lintegral_empty {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : α ennreal) :
∫⁻ (x : α) in , f x μ = 0
theorem measure_theory.set_lintegral_univ {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : α ennreal) :
∫⁻ (x : α) in set.univ, f x μ = ∫⁻ (x : α), f x μ
theorem measure_theory.set_lintegral_measure_zero {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (s : set α) (f : α ennreal) (hs' : μ s = 0) :
∫⁻ (x : α) in s, f x μ = 0
theorem measure_theory.lintegral_finset_sum' {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} (s : finset β) {f : β } (hf : (b : β), b s ae_measurable (f b) μ) :
∫⁻ (a : α), s.sum (λ (b : β), f b a) μ = s.sum (λ (b : β), ∫⁻ (a : α), f b a μ)
theorem measure_theory.lintegral_finset_sum {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} (s : finset β) {f : β } (hf : (b : β), b s measurable (f b)) :
∫⁻ (a : α), s.sum (λ (b : β), f b a) μ = s.sum (λ (b : β), ∫⁻ (a : α), f b a μ)
@[simp]
theorem measure_theory.lintegral_const_mul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (r : ennreal) {f : α ennreal} (hf : measurable f) :
∫⁻ (a : α), r * f a μ = r * ∫⁻ (a : α), f a μ
theorem measure_theory.lintegral_const_mul'' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (r : ennreal) {f : α ennreal} (hf : μ) :
∫⁻ (a : α), r * f a μ = r * ∫⁻ (a : α), f a μ
theorem measure_theory.lintegral_const_mul_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (r : ennreal) (f : α ennreal) :
r * ∫⁻ (a : α), f a μ ∫⁻ (a : α), r * f a μ
theorem measure_theory.lintegral_const_mul' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (r : ennreal) (f : α ennreal) (hr : r ) :
∫⁻ (a : α), r * f a μ = r * ∫⁻ (a : α), f a μ
theorem measure_theory.lintegral_mul_const {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (r : ennreal) {f : α ennreal} (hf : measurable f) :
∫⁻ (a : α), f a * r μ = ∫⁻ (a : α), f a μ * r
theorem measure_theory.lintegral_mul_const'' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (r : ennreal) {f : α ennreal} (hf : μ) :
∫⁻ (a : α), f a * r μ = ∫⁻ (a : α), f a μ * r
theorem measure_theory.lintegral_mul_const_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (r : ennreal) (f : α ennreal) :
∫⁻ (a : α), f a μ * r ∫⁻ (a : α), f a * r μ
theorem measure_theory.lintegral_mul_const' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (r : ennreal) (f : α ennreal) (hr : r ) :
∫⁻ (a : α), f a * r μ = ∫⁻ (a : α), f a μ * r
theorem measure_theory.lintegral_lintegral_mul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} {ν : measure_theory.measure β} {f : α ennreal} {g : β ennreal} (hf : μ) (hg : ν) :
∫⁻ (x : α), ∫⁻ (y : β), f x * g y ν μ = ∫⁻ (x : α), f x μ * ∫⁻ (y : β), g y ν
theorem measure_theory.lintegral_rw₁ {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f f' : α β} (h : f =ᵐ[μ] f') (g : β ennreal) :
∫⁻ (a : α), g (f a) μ = ∫⁻ (a : α), g (f' a) μ
theorem measure_theory.lintegral_rw₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} {f₁ f₁' : α β} {f₂ f₂' : α γ} (h₁ : f₁ =ᵐ[μ] f₁') (h₂ : f₂ =ᵐ[μ] f₂') (g : β ) :
∫⁻ (a : α), g (f₁ a) (f₂ a) μ = ∫⁻ (a : α), g (f₁' a) (f₂' a) μ
@[simp]
theorem measure_theory.lintegral_indicator {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : α ennreal) {s : set α} (hs : measurable_set s) :
∫⁻ (a : α), s.indicator f a μ = ∫⁻ (a : α) in s, f a μ
theorem measure_theory.lintegral_indicator₀ {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : α ennreal) {s : set α} (hs : μ) :
∫⁻ (a : α), s.indicator f a μ = ∫⁻ (a : α) in s, f a μ
theorem measure_theory.lintegral_indicator_const {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hs : measurable_set s) (c : ennreal) :
∫⁻ (a : α), s.indicator (λ (_x : α), c) a μ = c * μ s
theorem measure_theory.set_lintegral_eq_const {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (hf : measurable f) (r : ennreal) :
∫⁻ (x : α) in {x : α | f x = r}, f x μ = r * μ {x : α | f x = r}
@[simp]
theorem measure_theory.lintegral_indicator_one {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hs : measurable_set s) :
∫⁻ (a : α), s.indicator 1 a μ = μ s
theorem measure_theory.lintegral_add_mul_meas_add_le_le_lintegral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α ennreal} (hle : f ≤ᵐ[μ] g) (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 measure_theory.mul_meas_ge_le_lintegral₀ {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (hf : μ) (ε : ennreal) :
ε * μ {x : α | ε f x} ∫⁻ (a : α), f a μ

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

theorem measure_theory.mul_meas_ge_le_lintegral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (hf : measurable f) (ε : ennreal) :
ε * μ {x : α | ε f x} ∫⁻ (a : α), f a μ

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

theorem measure_theory.lintegral_eq_top_of_measure_eq_top_ne_zero {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (hf : μ) (hμf : μ {x : α | f x = } 0) :
∫⁻ (x : α), f x μ =
theorem measure_theory.set_lintegral_eq_top_of_measure_eq_top_ne_zero {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} {s : set α} (hf : (μ.restrict s)) (hμf : μ {x ∈ s | f x = } 0) :
∫⁻ (x : α) in s, f x μ =
theorem measure_theory.measure_eq_top_of_lintegral_ne_top {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (hf : μ) (hμf : ∫⁻ (x : α), f x μ ) :
μ {x : α | f x = } = 0
theorem measure_theory.measure_eq_top_of_set_lintegral_ne_top {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} {s : set α} (hf : (μ.restrict s)) (hμf : ∫⁻ (x : α) in s, f x μ ) :
μ {x ∈ s | f x = } = 0
theorem measure_theory.meas_ge_le_lintegral_div {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (hf : μ) {ε : ennreal} (hε : ε 0) (hε' : ε ) :
μ {x : α | ε f x} ∫⁻ (a : α), f a μ / ε

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

theorem measure_theory.ae_eq_of_ae_le_of_lintegral_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α ennreal} (hfg : f ≤ᵐ[μ] g) (hf : ∫⁻ (x : α), f x μ ) (hg : μ) (hgf : ∫⁻ (x : α), g x μ ∫⁻ (x : α), f x μ) :
f =ᵐ[μ] g
@[simp]
theorem measure_theory.lintegral_eq_zero_iff' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (hf : μ) :
∫⁻ (a : α), f a μ = 0 f =ᵐ[μ] 0
@[simp]
theorem measure_theory.lintegral_eq_zero_iff {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (hf : measurable f) :
∫⁻ (a : α), f a μ = 0 f =ᵐ[μ] 0
theorem measure_theory.lintegral_pos_iff_support {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (hf : measurable f) :
0 < ∫⁻ (a : α), f a μ 0 < μ
theorem measure_theory.lintegral_supr_ae {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : } (hf : (n : ), measurable (f n)) (h_mono : (n : ), ∀ᵐ (a : α) μ, f n a f n.succ a) :
∫⁻ (a : α), ( (n : ), f n a) μ = (n : ), ∫⁻ (a : α), f n a μ

Weaker version of the monotone convergence theorem

theorem measure_theory.lintegral_sub' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α ennreal} (hg : μ) (hg_fin : ∫⁻ (a : α), g a μ ) (h_le : g ≤ᵐ[μ] f) :
∫⁻ (a : α), f a - g a μ = ∫⁻ (a : α), f a μ - ∫⁻ (a : α), g a μ
theorem measure_theory.lintegral_sub {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α ennreal} (hg : measurable g) (hg_fin : ∫⁻ (a : α), g a μ ) (h_le : g ≤ᵐ[μ] f) :
∫⁻ (a : α), f a - g a μ = ∫⁻ (a : α), f a μ - ∫⁻ (a : α), g a μ
theorem measure_theory.lintegral_sub_le' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f g : α ennreal) (hf : μ) :
∫⁻ (x : α), g x μ - ∫⁻ (x : α), f x μ ∫⁻ (x : α), g x - f x μ
theorem measure_theory.lintegral_sub_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f g : α ennreal) (hf : measurable f) :
∫⁻ (x : α), g x μ - ∫⁻ (x : α), f x μ ∫⁻ (x : α), g x - f x μ
theorem measure_theory.lintegral_strict_mono_of_ae_le_of_frequently_ae_lt {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α ennreal} (hg : μ) (hfi : ∫⁻ (x : α), f x μ ) (h_le : f ≤ᵐ[μ] g) (h : ∃ᵐ (x : α) μ, f x g x) :
∫⁻ (x : α), f x μ < ∫⁻ (x : α), g x μ
theorem measure_theory.lintegral_strict_mono_of_ae_le_of_ae_lt_on {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α ennreal} (hg : μ) (hfi : ∫⁻ (x : α), f x μ ) (h_le : f ≤ᵐ[μ] g) {s : set α} (hμs : μ s 0) (h : ∀ᵐ (x : α) μ, x s f x < g x) :
∫⁻ (x : α), f x μ < ∫⁻ (x : α), g x μ
theorem measure_theory.lintegral_strict_mono {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α ennreal} (hμ : μ 0) (hg : μ) (hfi : ∫⁻ (x : α), f x μ ) (h : ∀ᵐ (x : α) μ, f x < g x) :
∫⁻ (x : α), f x μ < ∫⁻ (x : α), g x μ
theorem measure_theory.set_lintegral_strict_mono {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α ennreal} {s : set α} (hsm : measurable_set s) (hs : μ s 0) (hg : measurable g) (hfi : ∫⁻ (x : α) in s, f x μ ) (h : ∀ᵐ (x : α) μ, x s f x < g x) :
∫⁻ (x : α) in s, f x μ < ∫⁻ (x : α) in s, g x μ
theorem measure_theory.lintegral_infi_ae {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : } (h_meas : (n : ), measurable (f n)) (h_mono : (n : ), f n.succ ≤ᵐ[μ] 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 measure_theory.lintegral_infi {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : } (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 measure_theory.lintegral_liminf_le' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : } (h_meas : (n : ), ae_measurable (f n) μ) :
∫⁻ (a : α), filter.liminf (λ (n : ), f n a) filter.at_top μ filter.liminf (λ (n : ), ∫⁻ (a : α), f n a μ) filter.at_top

Known as Fatou's lemma, version with `ae_measurable` functions

theorem measure_theory.lintegral_liminf_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : } (h_meas : (n : ), measurable (f n)) :
∫⁻ (a : α), filter.liminf (λ (n : ), f n a) filter.at_top μ filter.liminf (λ (n : ), ∫⁻ (a : α), f n a μ) filter.at_top

Known as Fatou's lemma

theorem measure_theory.limsup_lintegral_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : } {g : α ennreal} (hf_meas : (n : ), measurable (f n)) (h_bound : (n : ), f n ≤ᵐ[μ] g) (h_fin : ∫⁻ (a : α), g a μ ) :
filter.limsup (λ (n : ), ∫⁻ (a : α), f n a μ) filter.at_top ∫⁻ (a : α), filter.limsup (λ (n : ), f n a) filter.at_top μ
theorem measure_theory.tendsto_lintegral_of_dominated_convergence {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {F : } {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 (λ (n : ), F n a) filter.at_top (nhds (f a))) :
filter.tendsto (λ (n : ), ∫⁻ (a : α), F n a μ) filter.at_top (nhds (∫⁻ (a : α), f a μ))

Dominated convergence theorem for nonnegative functions

theorem measure_theory.tendsto_lintegral_of_dominated_convergence' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {F : } {f : α ennreal} (bound : α ennreal) (hF_meas : (n : ), ae_measurable (F n) μ) (h_bound : (n : ), F n ≤ᵐ[μ] bound) (h_fin : ∫⁻ (a : α), bound a μ ) (h_lim : ∀ᵐ (a : α) μ, filter.tendsto (λ (n : ), F n a) filter.at_top (nhds (f a))) :
filter.tendsto (λ (n : ), ∫⁻ (a : α), F n a μ) filter.at_top (nhds (∫⁻ (a : α), f a μ))

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

theorem measure_theory.tendsto_lintegral_filter_of_dominated_convergence {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {ι : Type u_2} {l : filter ι} {F : ι } {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 (λ (n : ι), F n a) l (nhds (f a))) :
filter.tendsto (λ (n : ι), ∫⁻ (a : α), F n a μ) l (nhds (∫⁻ (a : α), f a μ))

Dominated convergence theorem for filters with a countable basis

theorem measure_theory.lintegral_supr_directed_of_measurable {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [countable β] {f : β } (hf : (b : β), measurable (f b)) (h_directed : 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 measure_theory.lintegral_supr_directed {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [countable β] {f : β } (hf : (b : β), ae_measurable (f b) μ) (h_directed : 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 measure_theory.lintegral_tsum {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [countable β] {f : β } (hf : (i : β), ae_measurable (f i) μ) :
∫⁻ (a : α), ∑' (i : β), f i a μ = ∑' (i : β), ∫⁻ (a : α), f i a μ
theorem measure_theory.lintegral_Union₀ {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [countable β] {s : β set α} (hm : (i : β), ) (hd : pairwise ) (f : α ennreal) :
∫⁻ (a : α) in (i : β), s i, f a μ = ∑' (i : β), ∫⁻ (a : α) in s i, f a μ
theorem measure_theory.lintegral_Union {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [countable β] {s : β set α} (hm : (i : β), measurable_set (s i)) (hd : pairwise (disjoint on s)) (f : α ennreal) :
∫⁻ (a : α) in (i : β), s i, f a μ = ∑' (i : β), ∫⁻ (a : α) in s i, f a μ
theorem measure_theory.lintegral_bUnion₀ {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {t : set β} {s : β set α} (ht : t.countable) (hm : (i : β), i t ) (hd : t.pairwise ) (f : α ennreal) :
∫⁻ (a : α) in (i : β) (H : i t), s i, f a μ = ∑' (i : t), ∫⁻ (a : α) in s i, f a μ
theorem measure_theory.lintegral_bUnion {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {t : set β} {s : β set α} (ht : t.countable) (hm : (i : β), i t measurable_set (s i)) (hd : t.pairwise_disjoint s) (f : α ennreal) :
∫⁻ (a : α) in (i : β) (H : i t), s i, f a μ = ∑' (i : t), ∫⁻ (a : α) in s i, f a μ
theorem measure_theory.lintegral_bUnion_finset₀ {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {s : finset β} {t : β set α} (hd : s.pairwise ) (hm : (b : β), b s ) (f : α ennreal) :
∫⁻ (a : α) in (b : β) (H : b s), t b, f a μ = s.sum (λ (b : β), ∫⁻ (a : α) in t b, f a μ)
theorem measure_theory.lintegral_bUnion_finset {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {s : finset β} {t : β set α} (hd : s.pairwise_disjoint t) (hm : (b : β), b s measurable_set (t b)) (f : α ennreal) :
∫⁻ (a : α) in (b : β) (H : b s), t b, f a μ = s.sum (λ (b : β), ∫⁻ (a : α) in t b, f a μ)
theorem measure_theory.lintegral_Union_le {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [countable β] (s : β set α) (f : α ennreal) :
∫⁻ (a : α) in (i : β), s i, f a μ ∑' (i : β), ∫⁻ (a : α) in s i, f a μ
theorem measure_theory.lintegral_union {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} {A B : set α} (hB : measurable_set B) (hAB : B) :
∫⁻ (a : α) in A B, f a μ = ∫⁻ (a : α) in A, f a μ + ∫⁻ (a : α) in B, f a μ
theorem measure_theory.lintegral_inter_add_diff {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {B : set α} (f : α ennreal) (A : set α) (hB : measurable_set B) :
∫⁻ (x : α) in A B, f x μ + ∫⁻ (x : α) in A \ B, f x μ = ∫⁻ (x : α) in A, f x μ
theorem measure_theory.lintegral_add_compl {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : α ennreal) {A : set α} (hA : measurable_set A) :
∫⁻ (x : α) in A, f x μ + ∫⁻ (x : α) in A, f x μ = ∫⁻ (x : α), f x μ
theorem measure_theory.lintegral_max {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α ennreal} (hf : measurable f) (hg : measurable g) :
∫⁻ (x : α), linear_order.max (f x) (g x) μ = ∫⁻ (x : α) in {x : α | f x g x}, g x μ + ∫⁻ (x : α) in {x : α | g x < f x}, f x μ
theorem measure_theory.set_lintegral_max {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α ennreal} (hf : measurable f) (hg : measurable g) (s : set α) :
∫⁻ (x : α) in s, linear_order.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 measure_theory.lintegral_map {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {mβ : measurable_space β} {f : β ennreal} {g : α β} (hf : measurable f) (hg : measurable g) :
∫⁻ (a : β), f a = ∫⁻ (a : α), f (g a) μ
theorem measure_theory.lintegral_map' {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {mβ : measurable_space β} {f : β ennreal} {g : α β} (hf : ) (hg : μ) :
∫⁻ (a : β), f a = ∫⁻ (a : α), f (g a) μ
theorem measure_theory.lintegral_map_le {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {mβ : measurable_space β} (f : β ennreal) {g : α β} (hg : measurable g) :
∫⁻ (a : β), f a ∫⁻ (a : α), f (g a) μ
theorem measure_theory.lintegral_comp {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : β ennreal} {g : α β} (hf : measurable f) (hg : measurable g) :
(f g) = ∫⁻ (a : β), f a
theorem measure_theory.set_lintegral_map {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : β ennreal} {g : α β} {s : set β} (hs : measurable_set s) (hf : measurable f) (hg : measurable g) :
∫⁻ (y : β) in s, f y = ∫⁻ (x : α) in g ⁻¹' s, f (g x) μ
theorem measure_theory.lintegral_indicator_const_comp {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {mβ : measurable_space β} {f : α β} {s : set β} (hf : measurable f) (hs : measurable_set s) (c : ennreal) :
∫⁻ (a : α), s.indicator (λ (_x : β), c) (f a) μ = c * μ (f ⁻¹' s)
theorem measurable_embedding.lintegral_map {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {g : α β} (hg : measurable_embedding g) (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` wich applies to any measurable `g : α → β` but requires that `f` is measurable as well.

theorem measure_theory.lintegral_map_equiv {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} (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 measure_theory.measure_preserving.lintegral_comp {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {mb : measurable_space β} {ν : measure_theory.measure β} {g : α β} (hg : ν) {f : β ennreal} (hf : measurable f) :
∫⁻ (a : α), f (g a) μ = ∫⁻ (b : β), f b ν
theorem measure_theory.measure_preserving.lintegral_comp_emb {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {mb : measurable_space β} {ν : measure_theory.measure β} {g : α β} (hg : ν) (hge : measurable_embedding g) (f : β ennreal) :
∫⁻ (a : α), f (g a) μ = ∫⁻ (b : β), f b ν
theorem measure_theory.measure_preserving.set_lintegral_comp_preimage {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {mb : measurable_space β} {ν : measure_theory.measure β} {g : α β} (hg : ν) {s : set β} (hs : measurable_set s) {f : β ennreal} (hf : measurable f) :
∫⁻ (a : α) in g ⁻¹' s, f (g a) μ = ∫⁻ (b : β) in s, f b ν
theorem measure_theory.measure_preserving.set_lintegral_comp_preimage_emb {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {mb : measurable_space β} {ν : measure_theory.measure β} {g : α β} (hg : ν) (hge : measurable_embedding g) (f : β ennreal) (s : set β) :
∫⁻ (a : α) in g ⁻¹' s, f (g a) μ = ∫⁻ (b : β) in s, f b ν
theorem measure_theory.measure_preserving.set_lintegral_comp_emb {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {mb : measurable_space β} {ν : measure_theory.measure β} {g : α β} (hg : ν) (hge : measurable_embedding g) (f : β ennreal) (s : set α) :
∫⁻ (a : α) in s, f (g a) μ = ∫⁻ (b : β) in g '' s, f b ν
@[protected, instance]
theorem measure_theory.lintegral_dirac' {α : Type u_1} (a : α) {f : α ennreal} (hf : measurable f) :
∫⁻ (a : α), f a = f a
theorem measure_theory.lintegral_dirac {α : Type u_1} (a : α) (f : α ennreal) :
∫⁻ (a : α), f a = f a
theorem measure_theory.set_lintegral_dirac' {α : Type u_1} {a : α} {f : α ennreal} (hf : measurable f) {s : set α} (hs : measurable_set s) [decidable (a s)] :
∫⁻ (x : α) in s, f x = ite (a s) (f a) 0
theorem measure_theory.set_lintegral_dirac {α : Type u_1} {a : α} (f : α ennreal) (s : set α) [decidable (a s)] :
∫⁻ (x : α) in s, f x = ite (a s) (f a) 0
theorem measure_theory.lintegral_count' {α : Type u_1} {f : α ennreal} (hf : measurable f) :
theorem measure_theory.lintegral_count {α : Type u_1} (f : α ennreal) :
theorem ennreal.tsum_const_eq {α : Type u_1} (c : ennreal) :
∑' (i : α), c =
theorem ennreal.count_const_le_le_of_tsum_le {α : Type u_1} {a : α ennreal} (a_mble : measurable a) {c : ennreal} (tsum_le_c : ∑' (i : α), a i c) {ε : ennreal} (ε_ne_zero : ε 0) (ε_ne_top : ε ) :
measure_theory.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 : measurable a) (a_summable : summable a) {c : nnreal} (tsum_le_c : ∑' (i : α), a i c) {ε : nnreal} (ε_ne_zero : ε 0) :

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

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

theorem measure_theory.lintegral_countable' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} [countable α] (f : α ennreal) :
∫⁻ (a : α), f a μ = ∑' (a : α), f a * μ {a}
theorem measure_theory.lintegral_singleton' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (hf : measurable f) (a : α) :
∫⁻ (x : α) in {a}, f x μ = f a * μ {a}
theorem measure_theory.lintegral_singleton {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : α ennreal) (a : α) :
∫⁻ (x : α) in {a}, f x μ = f a * μ {a}
theorem measure_theory.lintegral_countable {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : α ennreal) {s : set α} (hs : s.countable) :
∫⁻ (a : α) in s, f a μ = ∑' (a : s), f a * μ {a}
theorem measure_theory.lintegral_insert {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {a : α} {s : set α} (h : a s) (f : α ennreal) :
∫⁻ (x : α) in , f x μ = f a * μ {a} + ∫⁻ (x : α) in s, f x μ
theorem measure_theory.lintegral_finset {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (s : finset α) (f : α ennreal) :
∫⁻ (x : α) in s, f x μ = s.sum (λ (x : α), f x * μ {x})
theorem measure_theory.lintegral_fintype {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} [fintype α] (f : α ennreal) :
∫⁻ (x : α), f x μ = finset.univ.sum (λ (x : α), f x * μ {x})
theorem measure_theory.lintegral_unique {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} [unique α] (f : α ennreal) :
∫⁻ (x : α), f x μ =
theorem measure_theory.ae_lt_top {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (hf : measurable f) (h2f : ∫⁻ (x : α), f x μ ) :
∀ᵐ (x : α) μ, f x <
theorem measure_theory.ae_lt_top' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (hf : μ) (h2f : ∫⁻ (x : α), f x μ ) :
∀ᵐ (x : α) μ, f x <
theorem measure_theory.set_lintegral_lt_top_of_bdd_above {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hs : μ s ) {f : α nnreal} (hf : measurable f) (hbdd : bdd_above (f '' s)) :
∫⁻ (x : α) in s, (f x) μ <
theorem measure_theory.set_lintegral_lt_top_of_is_compact {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hs : μ s ) (hsc : is_compact s) {f : α nnreal} (hf : continuous f) :
∫⁻ (x : α) in s, (f x) μ <
theorem is_finite_measure.lintegral_lt_top_of_bounded_to_ennreal {α : Type u_1} (μ : measure_theory.measure α) [μ_fin : measure_theory.is_finite_measure μ] {f : α ennreal} (f_bdd : (c : nnreal), (x : α), f x c) :
∫⁻ (x : α), f x μ <
noncomputable def measure_theory.measure.with_density {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) (f : α ennreal) :

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

Equations
Instances for `measure_theory.measure.with_density`
@[simp]
theorem measure_theory.with_density_apply {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : α ennreal) {s : set α} (hs : measurable_set s) :
(μ.with_density f) s = ∫⁻ (a : α) in s, f a μ
theorem measure_theory.with_density_congr_ae {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α ennreal} (h : f =ᵐ[μ] g) :
theorem measure_theory.with_density_add_left {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (hf : measurable f) (g : α ennreal) :
theorem measure_theory.with_density_add_right {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : α ennreal) {g : α ennreal} (hg : measurable g) :
theorem measure_theory.with_density_sum {α : Type u_1} {ι : Type u_2} {m : measurable_space α} (μ : ι ) (f : α ennreal) :
= measure_theory.measure.sum (λ (n : ι), (μ n).with_density f)
theorem measure_theory.with_density_smul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (r : ennreal) {f : α ennreal} (hf : measurable f) :
theorem measure_theory.with_density_smul' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (r : ennreal) (f : α ennreal) (hr : r ) :
theorem measure_theory.is_finite_measure_with_density {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (hf : ∫⁻ (a : α), f a μ ) :
@[simp]
@[simp]
theorem measure_theory.with_density_tsum {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : } (h : (i : ), measurable (f i)) :
μ.with_density (∑' (n : ), f n) = measure_theory.measure.sum (λ (n : ), μ.with_density (f n))
theorem measure_theory.with_density_eq_zero {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (hf : μ) (h : μ.with_density f = 0) :
f =ᵐ[μ] 0
theorem measure_theory.with_density_apply_eq_zero {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} {s : set α} (hf : measurable f) :
(μ.with_density f) s = 0 μ ({x : α | f x 0} s) = 0
theorem measure_theory.ae_with_density_iff {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {p : α Prop} {f : α ennreal} (hf : measurable f) :
(∀ᵐ (x : α) μ.with_density f, p x) ∀ᵐ (x : α) μ, f x 0 p x
theorem measure_theory.ae_with_density_iff_ae_restrict {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {p : α Prop} {f : α ennreal} (hf : measurable f) :
(∀ᵐ (x : α) μ.with_density f, p x) ∀ᵐ (x : α) μ.restrict {x : α | f x 0}, p x
theorem measure_theory.ae_measurable_with_density_ennreal_iff {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α nnreal} (hf : measurable f) {g : α ennreal} :
(μ.with_density (λ (x : α), (f x))) ae_measurable (λ (x : α), (f x) * g x) μ
theorem measure_theory.lintegral_with_density_eq_lintegral_mul {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) {f : α ennreal} (h_mf : measurable f) {g : α ennreal} :
∫⁻ (a : α), g a μ.with_density f = ∫⁻ (a : α), (f * g) a μ

This is Exercise 1.2.1 from [Tao10]. It allows you to express integration of a measurable function with respect to `(μ.with_density 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 `(μ.with_density 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 measure_theory.set_lintegral_with_density_eq_set_lintegral_mul {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) {f g : α ennreal} (hf : measurable f) (hg : measurable g) {s : set α} (hs : measurable_set s) :
∫⁻ (x : α) in s, g x μ.with_density f = ∫⁻ (x : α) in s, (f * g) x μ
theorem measure_theory.lintegral_with_density_eq_lintegral_mul₀' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (hf : μ) {g : α ennreal} (hg : (μ.with_density f)) :
∫⁻ (a : α), g a μ.with_density f = ∫⁻ (a : α), (f * g) a μ

The Lebesgue integral of `g` with respect to the measure `μ.with_density 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_with_density_eq_lintegral_mul_non_measurable`

theorem measure_theory.lintegral_with_density_eq_lintegral_mul₀ {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (hf : μ) {g : α ennreal} (hg : μ) :
∫⁻ (a : α), g a μ.with_density f = ∫⁻ (a : α), (f * g) a μ
theorem measure_theory.lintegral_with_density_le_lintegral_mul {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) {f : α ennreal} (f_meas : measurable f) (g : α ennreal) :
∫⁻ (a : α), g a μ.with_density f ∫⁻ (a : α), (f * g) a μ
theorem measure_theory.lintegral_with_density_eq_lintegral_mul_non_measurable {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) {f : α ennreal} (f_meas : measurable f) (hf : ∀ᵐ (x : α) μ, f x < ) (g : α ennreal) :
∫⁻ (a : α), g a μ.with_density f = ∫⁻ (a : α), (f * g) a μ
theorem measure_theory.set_lintegral_with_density_eq_set_lintegral_mul_non_measurable {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) {f : α ennreal} (f_meas : measurable f) (g : α ennreal) {s : set α} (hs : measurable_set s) (hf : ∀ᵐ (x : α) μ.restrict s, f x < ) :
∫⁻ (a : α) in s, g a μ.with_density f = ∫⁻ (a : α) in s, (f * g) a μ
theorem measure_theory.lintegral_with_density_eq_lintegral_mul_non_measurable₀ {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) {f : α ennreal} (hf : μ) (h'f : ∀ᵐ (x : α) μ, f x < ) (g : α ennreal) :
∫⁻ (a : α), g a μ.with_density f = ∫⁻ (a : α), (f * g) a μ
theorem measure_theory.set_lintegral_with_density_eq_set_lintegral_mul_non_measurable₀ {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) {f : α ennreal} {s : set α} (hf : (μ.restrict s)) (g : α ennreal) (hs : measurable_set s) (h'f : ∀ᵐ (x : α) μ.restrict s, f x < ) :
∫⁻ (a : α) in s, g a μ.with_density f = ∫⁻ (a : α) in s, (f * g) a μ
theorem measure_theory.with_density_mul {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) {f g : α ennreal} (hf : measurable f) (hg : measurable g) :
theorem measure_theory.exists_pos_lintegral_lt_of_sigma_finite {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) {ε : ennreal} (ε0 : ε 0) :
(g : α nnreal), ( (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 measure_theory.lintegral_trim {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) {f : α ennreal} (hf : measurable f) :
∫⁻ (a : α), f a μ.trim hm = ∫⁻ (a : α), f a μ
theorem measure_theory.lintegral_trim_ae {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) {f : α ennreal} (hf : (μ.trim hm)) :
∫⁻ (a : α), f a μ.trim hm = ∫⁻ (a : α), f a μ
theorem measure_theory.univ_le_of_forall_fin_meas_le {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] (C : ennreal) {f : set α ennreal} (hf : (s : set α), μ s f s C) (h_F_lim : (S : set α), ( (n : ), measurable_set (S n)) (f ( (n : ), S n) (n : ), f (S n))) :
C
theorem measure_theory.lintegral_le_of_forall_fin_meas_le_of_measurable {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] (C : ennreal) {f : α ennreal} (hf_meas : measurable f) (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 `ae_measurable` version.

theorem measure_theory.lintegral_le_of_forall_fin_meas_le' {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] (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 measure_theory.lintegral_le_of_forall_fin_meas_le {α : Type u_1} {μ : measure_theory.measure α} (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 measure_theory.simple_func.exists_lt_lintegral_simple_func_of_lt_lintegral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {L : ennreal} (hL : L < ∫⁻ (x : α), (f x) μ) :
(g : , ( (x : α), g x f x) ∫⁻ (x : α), (g x) μ < L < ∫⁻ (x : α), (g x) μ
theorem measure_theory.exists_lt_lintegral_simple_func_of_lt_lintegral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {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.