# mathlibdocumentation

measure_theory.integration

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

We define simple functions and show that each Borel measurable function on `ℝ≥0∞` can be approximated by a sequence of simple functions.

To prove something for an arbitrary measurable function into `ℝ≥0∞`, the theorem `measurable.ennreal_induction` shows that is it sufficient to show that the property holds for (multiples of) characteristic functions and is closed under addition and supremum of increasing sequences of functions.

## 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)`.
structure measure_theory.simple_func (α : Type u) (β : Type v) :
Type (max u v)

A function `f` from a measurable space to any type is called simple, if every preimage `f ⁻¹' {x}` is measurable, and the range is finite. This structure bundles a function with these properties.

@[instance]
def measure_theory.simple_func.has_coe_to_fun {α : Type u_1} {β : Type u_2}  :
Equations
theorem measure_theory.simple_func.coe_injective {α : Type u_1} {β : Type u_2} ⦃f g : β⦄ (H : f = g) :
f = g
@[ext]
theorem measure_theory.simple_func.ext {α : Type u_1} {β : Type u_2} {f g : β} (H : ∀ (a : α), f a = g a) :
f = g
theorem measure_theory.simple_func.finite_range {α : Type u_1} {β : Type u_2} (f : β) :
theorem measure_theory.simple_func.measurable_set_fiber {α : Type u_1} {β : Type u_2} (f : β) (x : β) :
def measure_theory.simple_func.range {α : Type u_1} {β : Type u_2} (f : β) :

Range of a simple function `α →ₛ β` as a `finset β`.

Equations
@[simp]
theorem measure_theory.simple_func.mem_range {α : Type u_1} {β : Type u_2} {f : β} {b : β} :
b f.range b
theorem measure_theory.simple_func.mem_range_self {α : Type u_1} {β : Type u_2} (f : β) (x : α) :
@[simp]
theorem measure_theory.simple_func.coe_range {α : Type u_1} {β : Type u_2} (f : β) :
(f.range) =
theorem measure_theory.simple_func.mem_range_of_measure_ne_zero {α : Type u_1} {β : Type u_2} {f : β} {x : β} {μ : measure_theory.measure α} (H : μ (f ⁻¹' {x}) 0) :
theorem measure_theory.simple_func.forall_range_iff {α : Type u_1} {β : Type u_2} {f : β} {p : β → Prop} :
(∀ (y : β), y f.rangep y) ∀ (x : α), p (f x)
theorem measure_theory.simple_func.exists_range_iff {α : Type u_1} {β : Type u_2} {f : β} {p : β → Prop} :
(∃ (y : β) (H : y f.range), p y) ∃ (x : α), p (f x)
theorem measure_theory.simple_func.preimage_eq_empty_iff {α : Type u_1} {β : Type u_2} (f : β) (b : β) :
theorem measure_theory.simple_func.exists_forall_le {α : Type u_1} {β : Type u_2} [nonempty β] (f : β) :
∃ (C : β), ∀ (x : α), f x C
def measure_theory.simple_func.const (α : Type u_1) {β : Type u_2} (b : β) :

Constant function as a `simple_func`.

Equations
@[instance]
def measure_theory.simple_func.inhabited {α : Type u_1} {β : Type u_2} [inhabited β] :
Equations
theorem measure_theory.simple_func.const_apply {α : Type u_1} {β : Type u_2} (a : α) (b : β) :
= b
@[simp]
theorem measure_theory.simple_func.coe_const {α : Type u_1} {β : Type u_2} (b : β) :
@[simp]
theorem measure_theory.simple_func.range_const {β : Type u_2} (α : Type u_1) [nonempty α] (b : β) :
= {b}
theorem measure_theory.simple_func.measurable_set_cut {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (f : β) (h : ∀ (b : β), measurable_set {a : α | r a b}) :
measurable_set {a : α | r a (f a)}
theorem measure_theory.simple_func.measurable_set_preimage {α : Type u_1} {β : Type u_2} (f : β) (s : set β) :
theorem measure_theory.simple_func.measurable {α : Type u_1} {β : Type u_2} (f : β) :

A simple function is measurable

theorem measure_theory.simple_func.ae_measurable {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f : β) :
theorem measure_theory.simple_func.sum_measure_preimage_singleton {α : Type u_1} {β : Type u_2} (f : β) {μ : measure_theory.measure α} (s : finset β) :
∑ (y : β) in s, μ (f ⁻¹' {y}) = μ (f ⁻¹' s)
theorem measure_theory.simple_func.sum_range_measure_preimage_singleton {α : Type u_1} {β : Type u_2} (f : β) (μ : measure_theory.measure α) :
∑ (y : β) in f.range, μ (f ⁻¹' {y}) =
def measure_theory.simple_func.piecewise {α : Type u_1} {β : Type u_2} (s : set α) (hs : measurable_set s) (f g : β) :

If-then-else as a `simple_func`.

Equations
@[simp]
theorem measure_theory.simple_func.coe_piecewise {α : Type u_1} {β : Type u_2} {s : set α} (hs : measurable_set s) (f g : β) :
theorem measure_theory.simple_func.piecewise_apply {α : Type u_1} {β : Type u_2} {s : set α} (hs : measurable_set s) (f g : β) (a : α) :
g) a = ite (a s) (f a) (g a)
@[simp]
theorem measure_theory.simple_func.piecewise_compl {α : Type u_1} {β : Type u_2} {s : set α} (hs : measurable_set s) (f g : β) :
@[simp]
theorem measure_theory.simple_func.piecewise_univ {α : Type u_1} {β : Type u_2} (f g : β) :
@[simp]
theorem measure_theory.simple_func.piecewise_empty {α : Type u_1} {β : Type u_2} (f g : β) :
theorem measure_theory.simple_func.support_indicator {α : Type u_1} {β : Type u_2} [has_zero β] {s : set α} (hs : measurable_set s) (f : β) :
theorem measure_theory.simple_func.measurable_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β) (g : β → α → γ) (hg : ∀ (b : β), measurable (g b)) :
measurable (λ (a : α), g (f a) a)
def measure_theory.simple_func.bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β) (g : β → ) :

If `f : α →ₛ β` is a simple function and `g : β → α →ₛ γ` is a family of simple functions, then `f.bind g` binds the first argument of `g` to `f`. In other words, `f.bind g a = g (f a) a`.

Equations
@[simp]
theorem measure_theory.simple_func.bind_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β) (g : β → ) (a : α) :
(f.bind g) a = (g (f a)) a
def measure_theory.simple_func.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : β) :

Given a function `g : β → γ` and a simple function `f : α →ₛ β`, `f.map g` return the simple function `g ∘ f : α →ₛ γ`

Equations
theorem measure_theory.simple_func.map_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : β) (a : α) :
= g (f a)
theorem measure_theory.simple_func.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (g : β → γ) (h : γ → δ) (f : β) :
@[simp]
theorem measure_theory.simple_func.coe_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : β) :
= g f
@[simp]
theorem measure_theory.simple_func.range_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq γ] (g : β → γ) (f : β) :
@[simp]
theorem measure_theory.simple_func.map_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (b : β) :
theorem measure_theory.simple_func.map_preimage {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β) (g : β → γ) (s : set γ) :
= f ⁻¹' (finset.filter (λ (b : β), g b s) f.range)
theorem measure_theory.simple_func.map_preimage_singleton {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β) (g : β → γ) (c : γ) :
⁻¹' {c} = f ⁻¹' (finset.filter (λ (b : β), g b = c) f.range)
def measure_theory.simple_func.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : γ) (g : α → β) (hgm : measurable g) :

Composition of a `simple_fun` and a measurable function is a `simple_func`.

Equations
@[simp]
theorem measure_theory.simple_func.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : γ) {g : α → β} (hgm : measurable g) :
(f.comp g hgm) = f g
theorem measure_theory.simple_func.range_comp_subset_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : γ) {g : α → β} (hgm : measurable g) :
(f.comp g hgm).range f.range
def measure_theory.simple_func.seq {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : (β → γ)) (g : β) :

If `f` is a simple function taking values in `β → γ` and `g` is another simple function with the same domain and codomain `β`, then `f.seq g = f a (g a)`.

Equations
@[simp]
theorem measure_theory.simple_func.seq_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : (β → γ)) (g : β) (a : α) :
(f.seq g) a = f a (g a)
def measure_theory.simple_func.pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β) (g : γ) :
× γ)

Combine two simple functions `f : α →ₛ β` and `g : α →ₛ β` into `λ a, (f a, g a)`.

Equations
@[simp]
theorem measure_theory.simple_func.pair_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β) (g : γ) (a : α) :
(f.pair g) a = (f a, g a)
theorem measure_theory.simple_func.pair_preimage {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β) (g : γ) (s : set β) (t : set γ) :
theorem measure_theory.simple_func.pair_preimage_singleton {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β) (g : γ) (b : β) (c : γ) :
(f.pair g) ⁻¹' {(b, c)} = f ⁻¹' {b} g ⁻¹' {c}
theorem measure_theory.simple_func.bind_const {α : Type u_1} {β : Type u_2} (f : β) :
@[instance]
def measure_theory.simple_func.has_zero {α : Type u_1} {β : Type u_2} [has_zero β] :
Equations
@[instance]
def measure_theory.simple_func.has_add {α : Type u_1} {β : Type u_2} [has_add β] :
Equations
@[instance]
def measure_theory.simple_func.has_mul {α : Type u_1} {β : Type u_2} [has_mul β] :
Equations
@[instance]
def measure_theory.simple_func.has_sup {α : Type u_1} {β : Type u_2} [has_sup β] :
Equations
@[instance]
def measure_theory.simple_func.has_inf {α : Type u_1} {β : Type u_2} [has_inf β] :
Equations
@[instance]
def measure_theory.simple_func.has_le {α : Type u_1} {β : Type u_2} [has_le β] :
Equations
@[simp]
theorem measure_theory.simple_func.coe_zero {α : Type u_1} {β : Type u_2} [has_zero β] :
0 = 0
@[simp]
theorem measure_theory.simple_func.const_zero {α : Type u_1} {β : Type u_2} [has_zero β] :
@[simp]
theorem measure_theory.simple_func.coe_add {α : Type u_1} {β : Type u_2} [has_add β] (f g : β) :
(f + g) = f + g
@[simp]
theorem measure_theory.simple_func.coe_mul {α : Type u_1} {β : Type u_2} [has_mul β] (f g : β) :
f * g = (f) * g
@[simp]
theorem measure_theory.simple_func.coe_le {α : Type u_1} {β : Type u_2} [preorder β] {f g : β} :
f g f g
@[simp]
theorem measure_theory.simple_func.range_zero {α : Type u_1} {β : Type u_2} [nonempty α] [has_zero β] :
0.range = {0}
theorem measure_theory.simple_func.eq_zero_of_mem_range_zero {α : Type u_1} {β : Type u_2} [has_zero β] {y : β} :
y 0.rangey = 0
theorem measure_theory.simple_func.sup_apply {α : Type u_1} {β : Type u_2} [has_sup β] (f g : β) (a : α) :
(f g) a = f a g a
theorem measure_theory.simple_func.mul_apply {α : Type u_1} {β : Type u_2} [has_mul β] (f g : β) (a : α) :
(f * g) a = (f a) * g a
theorem measure_theory.simple_func.add_apply {α : Type u_1} {β : Type u_2} [has_add β] (f g : β) (a : α) :
(f + g) a = f a + g a
theorem measure_theory.simple_func.add_eq_map₂ {α : Type u_1} {β : Type u_2} [has_add β] (f g : β) :
f + g = measure_theory.simple_func.map (λ (p : β × β), p.fst + p.snd) (f.pair g)
theorem measure_theory.simple_func.mul_eq_map₂ {α : Type u_1} {β : Type u_2} [has_mul β] (f g : β) :
f * g = measure_theory.simple_func.map (λ (p : β × β), (p.fst) * p.snd) (f.pair g)
theorem measure_theory.simple_func.sup_eq_map₂ {α : Type u_1} {β : Type u_2} [has_sup β] (f g : β) :
f g = measure_theory.simple_func.map (λ (p : β × β), p.fst p.snd) (f.pair g)
theorem measure_theory.simple_func.const_mul_eq_map {α : Type u_1} {β : Type u_2} [has_mul β] (f : β) (b : β) :
= measure_theory.simple_func.map (λ (a : β), b * a) f
theorem measure_theory.simple_func.map_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_add β] [has_add γ] {g : β → γ} (hg : ∀ (x y : β), g (x + y) = g x + g y) (f₁ f₂ : β) :
@[instance]
def measure_theory.simple_func.add_monoid {α : Type u_1} {β : Type u_2} [add_monoid β] :
Equations
@[instance]
def measure_theory.simple_func.add_comm_monoid {α : Type u_1} {β : Type u_2}  :
Equations
@[instance]
def measure_theory.simple_func.has_neg {α : Type u_1} {β : Type u_2} [has_neg β] :
Equations
@[simp]
theorem measure_theory.simple_func.coe_neg {α : Type u_1} {β : Type u_2} [has_neg β] (f : β) :
@[instance]
def measure_theory.simple_func.has_sub {α : Type u_1} {β : Type u_2} [has_sub β] :
Equations
@[simp]
theorem measure_theory.simple_func.coe_sub {α : Type u_1} {β : Type u_2} [has_sub β] (f g : β) :
(f - g) = f - g
theorem measure_theory.simple_func.sub_apply {α : Type u_1} {β : Type u_2} [has_sub β] (f g : β) (x : α) :
(f - g) x = f x - g x
@[instance]
def measure_theory.simple_func.add_group {α : Type u_1} {β : Type u_2} [add_group β] :
Equations
@[instance]
def measure_theory.simple_func.add_comm_group {α : Type u_1} {β : Type u_2}  :
Equations
@[instance]
def measure_theory.simple_func.has_scalar {α : Type u_1} {β : Type u_2} {K : Type u_5} [ β] :
Equations
@[simp]
theorem measure_theory.simple_func.coe_smul {α : Type u_1} {β : Type u_2} {K : Type u_5} [ β] (c : K) (f : β) :
(c f) = c f
theorem measure_theory.simple_func.smul_apply {α : Type u_1} {β : Type u_2} {K : Type u_5} [ β] (k : K) (f : β) (a : α) :
(k f) a = k f a
@[instance]
def measure_theory.simple_func.module {α : Type u_1} {β : Type u_2} {K : Type u_5} [semiring K] [ β] :
Equations
theorem measure_theory.simple_func.smul_eq_map {α : Type u_1} {β : Type u_2} {K : Type u_5} [ β] (k : K) (f : β) :
@[instance]
def measure_theory.simple_func.preorder {α : Type u_1} {β : Type u_2} [preorder β] :
Equations
@[instance]
def measure_theory.simple_func.partial_order {α : Type u_1} {β : Type u_2}  :
Equations
@[instance]
def measure_theory.simple_func.order_bot {α : Type u_1} {β : Type u_2} [order_bot β] :
Equations
@[instance]
def measure_theory.simple_func.order_top {α : Type u_1} {β : Type u_2} [order_top β] :
Equations
@[instance]
def measure_theory.simple_func.semilattice_inf {α : Type u_1} {β : Type u_2}  :
Equations
@[instance]
def measure_theory.simple_func.semilattice_sup {α : Type u_1} {β : Type u_2}  :
Equations
@[instance]
def measure_theory.simple_func.semilattice_sup_bot {α : Type u_1} {β : Type u_2}  :
Equations
@[instance]
def measure_theory.simple_func.lattice {α : Type u_1} {β : Type u_2} [lattice β] :
Equations
@[instance]
def measure_theory.simple_func.bounded_lattice {α : Type u_1} {β : Type u_2}  :
Equations
theorem measure_theory.simple_func.finset_sup_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : γ → } (s : finset γ) (a : α) :
(s.sup f) a = s.sup (λ (c : γ), (f c) a)
def measure_theory.simple_func.restrict {α : Type u_1} {β : Type u_2} [has_zero β] (f : β) (s : set α) :

Restrict a simple function `f : α →ₛ β` to a set `s`. If `s` is measurable, then `f.restrict s a = if a ∈ s then f a else 0`, otherwise `f.restrict s = const α 0`.

Equations
• f.restrict s = (λ (hs : , 0) (λ (hs : , 0)
theorem measure_theory.simple_func.restrict_of_not_measurable {α : Type u_1} {β : Type u_2} [has_zero β] {f : β} {s : set α} (hs : ¬) :
f.restrict s = 0
@[simp]
theorem measure_theory.simple_func.coe_restrict {α : Type u_1} {β : Type u_2} [has_zero β] (f : β) {s : set α} (hs : measurable_set s) :
@[simp]
theorem measure_theory.simple_func.restrict_univ {α : Type u_1} {β : Type u_2} [has_zero β] (f : β) :
@[simp]
theorem measure_theory.simple_func.restrict_empty {α : Type u_1} {β : Type u_2} [has_zero β] (f : β) :
= 0
theorem measure_theory.simple_func.map_restrict_of_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero β] [has_zero γ] {g : β → γ} (hg : g 0 = 0) (f : β) (s : set α) :
theorem measure_theory.simple_func.map_coe_ennreal_restrict {α : Type u_1} (s : set α) :
theorem measure_theory.simple_func.map_coe_nnreal_restrict {α : Type u_1} (s : set α) :
theorem measure_theory.simple_func.restrict_apply {α : Type u_1} {β : Type u_2} [has_zero β] (f : β) {s : set α} (hs : measurable_set s) (a : α) :
(f.restrict s) a = s.indicator f a
theorem measure_theory.simple_func.restrict_preimage {α : Type u_1} {β : Type u_2} [has_zero β] (f : β) {s : set α} (hs : measurable_set s) {t : set β} (ht : 0 t) :
theorem measure_theory.simple_func.restrict_preimage_singleton {α : Type u_1} {β : Type u_2} [has_zero β] (f : β) {s : set α} (hs : measurable_set s) {r : β} (hr : r 0) :
(f.restrict s) ⁻¹' {r} = s f ⁻¹' {r}
theorem measure_theory.simple_func.mem_restrict_range {α : Type u_1} {β : Type u_2} [has_zero β] {r : β} {s : set α} {f : β} (hs : measurable_set s) :
r (f.restrict s).range r = 0 r f '' s
theorem measure_theory.simple_func.mem_image_of_mem_range_restrict {α : Type u_1} {β : Type u_2} [has_zero β] {r : β} {s : set α} {f : β} (hr : r (f.restrict s).range) (h0 : r 0) :
r f '' s
theorem measure_theory.simple_func.restrict_mono {α : Type u_1} {β : Type u_2} [has_zero β] [preorder β] (s : set α) {f g : β} (H : f g) :
def measure_theory.simple_func.approx {α : Type u_1} {β : Type u_2} [has_zero β] (i : → β) (f : α → β) (n : ) :

Fix a sequence `i : ℕ → β`. Given a function `α → β`, its `n`-th approximation by simple functions is defined so that in case `β = ℝ≥0∞` it sends each `a` to the supremum of the set `{i k | k ≤ n ∧ i k ≤ f a}`, see `approx_apply` and `supr_approx_apply` for details.

Equations
theorem measure_theory.simple_func.approx_apply {α : Type u_1} {β : Type u_2} [has_zero β] {i : → β} {f : α → β} {n : } (a : α) (hf : measurable f) :
a = (finset.range n).sup (λ (k : ), ite (i k f a) (i k) 0)
theorem measure_theory.simple_func.monotone_approx {α : Type u_1} {β : Type u_2} [has_zero β] (i : → β) (f : α → β) :
theorem measure_theory.simple_func.approx_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero β] {i : → β} {f : γ → β} {g : α → γ} {n : } (a : α) (hf : measurable f) (hg : measurable g) :
(f g) n) a = (g a)
theorem measure_theory.simple_func.supr_approx_apply {α : Type u_1} {β : Type u_2} [has_zero β] (i : → β) (f : α → β) (a : α) (hf : measurable f) (h_zero : 0 = ) :
(⨆ (n : ), a) = ⨆ (k : ) (h : i k f a), i k

A sequence of `ℝ≥0∞`s such that its range is the set of non-negative rational numbers.

Equations
def measure_theory.simple_func.eapprox {α : Type u_1}  :
(α → ℝ≥0∞)

Approximate a function `α → ℝ≥0∞` by a sequence of simple functions.

Equations
theorem measure_theory.simple_func.eapprox_lt_top {α : Type u_1} (f : α → ℝ≥0∞) (n : ) (a : α) :
theorem measure_theory.simple_func.monotone_eapprox {α : Type u_1} (f : α → ℝ≥0∞) :
theorem measure_theory.simple_func.supr_eapprox_apply {α : Type u_1} (f : α → ℝ≥0∞) (hf : measurable f) (a : α) :
(⨆ (n : ), = f a
theorem measure_theory.simple_func.eapprox_comp {α : Type u_1} {γ : Type u_3} {f : γ → ℝ≥0∞} {g : α → γ} {n : } (hf : measurable f) (hg : measurable g) :
n) =
def measure_theory.simple_func.eapprox_diff {α : Type u_1} (f : α → ℝ≥0∞) (n : ) :

Approximate a function `α → ℝ≥0∞` by a series of simple functions taking their values in `ℝ≥0`.

Equations
theorem measure_theory.simple_func.sum_eapprox_diff {α : Type u_1} (f : α → ℝ≥0∞) (n : ) (a : α) :
∑ (k : ) in finset.range (n + 1), =
theorem measure_theory.simple_func.tsum_eapprox_diff {α : Type u_1} (f : α → ℝ≥0∞) (hf : measurable f) (a : α) :
∑' (n : ), = f a

Integral of a simple function whose codomain is `ℝ≥0∞`.

Equations
theorem measure_theory.simple_func.lintegral_eq_of_subset {α : Type u_1} {μ : measure_theory.measure α} {s : finset ℝ≥0∞} (hs : ∀ (x : α), f x 0μ (f ⁻¹' {f x}) 0f x s) :
f.lintegral μ = ∑ (x : ℝ≥0∞) in s, x * μ (f ⁻¹' {x})
theorem measure_theory.simple_func.map_lintegral {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (g : β → ℝ≥0∞) (f : β) :
= ∑ (x : β) in f.range, (g x) * μ (f ⁻¹' {x})

Calculate the integral of `(g ∘ f)`, where `g : β → ℝ≥0∞` and `f : α →ₛ β`.

theorem measure_theory.simple_func.add_lintegral {α : Type u_1} {μ : measure_theory.measure α} (f g : ℝ≥0∞) :
(f + g).lintegral μ = f.lintegral μ + g.lintegral μ

Integral of a simple function `α →ₛ ℝ≥0∞` as a bilinear map.

Equations
@[simp]
theorem measure_theory.simple_func.zero_lintegral {α : Type u_1} {μ : measure_theory.measure α} :
0.lintegral μ = 0
theorem measure_theory.simple_func.lintegral_add {α : Type u_1} {μ ν : measure_theory.measure α}  :
f.lintegral + ν) = f.lintegral μ + f.lintegral ν
@[simp]
theorem measure_theory.simple_func.lintegral_zero {α : Type u_1}  :
f.lintegral 0 = 0
theorem measure_theory.simple_func.lintegral_sum {α : Type u_1} {ι : Type u_2} (μ : ι → ) :
= ∑' (i : ι), f.lintegral (μ i)
theorem measure_theory.simple_func.restrict_lintegral {α : Type u_1} {μ : measure_theory.measure α} {s : set α} (hs : measurable_set s) :
(f.restrict s).lintegral μ = ∑ (r : ℝ≥0∞) in f.range, r * μ (f ⁻¹' {r} s)
theorem measure_theory.simple_func.lintegral_restrict {α : Type u_1} (s : set α) (μ : measure_theory.measure α) :
f.lintegral (μ.restrict s) = ∑ (y : ℝ≥0∞) in f.range, y * μ (f ⁻¹' {y} s)
theorem measure_theory.simple_func.const_lintegral_restrict {α : Type u_1} {μ : measure_theory.measure α} (c : ℝ≥0∞) (s : set α) :
(μ.restrict s) = c * μ s
theorem measure_theory.simple_func.restrict_const_lintegral {α : Type u_1} {μ : measure_theory.measure α} (c : ℝ≥0∞) {s : set α} (hs : measurable_set s) :
μ = c * μ s
theorem measure_theory.simple_func.lintegral_mono {α : Type u_1} {f g : ℝ≥0∞} (hfg : f g) {μ ν : measure_theory.measure α} (hμν : μ ν) :

`simple_func.lintegral` is monotone both in function and in measure.

theorem measure_theory.simple_func.lintegral_eq_of_measure_preimage {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {ν : measure_theory.measure β} (H : ∀ (y : ℝ≥0∞), μ (f ⁻¹' {y}) = ν (g ⁻¹' {y})) :

`simple_func.lintegral` depends only on the measures of `f ⁻¹' {y}`.

theorem measure_theory.simple_func.lintegral_congr {α : Type u_1} {μ : measure_theory.measure α} {f g : ℝ≥0∞} (h : f =ᵐ[μ] g) :

If two simple functions are equal a.e., then their `lintegral`s are equal.

theorem measure_theory.simple_func.lintegral_map {α : Type u_1} {μ : measure_theory.measure α} {β : Type u_2} {μ' : measure_theory.measure β} (m : α → β) (eq : ∀ (a : α), f a = g (m a)) (h : ∀ (s : set β), μ' s = μ (m ⁻¹' s)) :
f.lintegral μ = g.lintegral μ'
theorem measure_theory.simple_func.lintegral_map_equiv {α : Type u_1} {μ : measure_theory.measure α} {β : Type u_2} (m : α ≃ᵐ β) :
(g.comp m _).lintegral μ = g.lintegral μ)

The `lintegral` of simple functions transforms appropriately under a measurable equivalence. (Compare `lintegral_map`, which applies to a broader class of transformations of the domain, but requires measurability of the function being integrated.)

theorem measure_theory.simple_func.support_eq {α : Type u_1} {β : Type u_2} [has_zero β] (f : β) :
= ⋃ (y : β) (H : y finset.filter (λ (y : β), y 0) f.range), f ⁻¹' {y}
def measure_theory.simple_func.fin_meas_supp {α : Type u_1} {β : Type u_2} [has_zero β] (f : β) (μ : measure_theory.measure α) :
Prop

A `simple_func` has finite measure support if it is equal to `0` outside of a set of finite measure.

Equations
theorem measure_theory.simple_func.fin_meas_supp_iff_support {α : Type u_1} {β : Type u_2} [has_zero β] {f : β} {μ : measure_theory.measure α} :
theorem measure_theory.simple_func.fin_meas_supp_iff {α : Type u_1} {β : Type u_2} [has_zero β] {f : β} {μ : measure_theory.measure α} :
∀ (y : β), y 0μ (f ⁻¹' {y}) <
theorem measure_theory.simple_func.fin_meas_supp.meas_preimage_singleton_ne_zero {α : Type u_1} {β : Type u_2} [has_zero β] {μ : measure_theory.measure α} {f : β} (h : f.fin_meas_supp μ) {y : β} (hy : y 0) :
μ (f ⁻¹' {y}) <
theorem measure_theory.simple_func.fin_meas_supp.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero β] [has_zero γ] {μ : measure_theory.measure α} {f : β} {g : β → γ} (hf : f.fin_meas_supp μ) (hg : g 0 = 0) :
theorem measure_theory.simple_func.fin_meas_supp.of_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero β] [has_zero γ] {μ : measure_theory.measure α} {f : β} {g : β → γ} (h : μ) (hg : ∀ (b : β), g b = 0b = 0) :
theorem measure_theory.simple_func.fin_meas_supp.map_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero β] [has_zero γ] {μ : measure_theory.measure α} {f : β} {g : β → γ} (hg : ∀ {b : β}, g b = 0 b = 0) :
theorem measure_theory.simple_func.fin_meas_supp.pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero β] [has_zero γ] {μ : measure_theory.measure α} {f : β} {g : γ} (hf : f.fin_meas_supp μ) (hg : g.fin_meas_supp μ) :
theorem measure_theory.simple_func.fin_meas_supp.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [has_zero β] [has_zero γ] [has_zero δ] {μ : measure_theory.measure α} {f : β} (hf : f.fin_meas_supp μ) {g : γ} (hg : g.fin_meas_supp μ) {op : β → γ → δ} (H : op 0 0 = 0) :
(f.pair g)).fin_meas_supp μ
theorem measure_theory.simple_func.fin_meas_supp.add {α : Type u_1} {μ : measure_theory.measure α} {β : Type u_2} [add_monoid β] {f g : β} (hf : f.fin_meas_supp μ) (hg : g.fin_meas_supp μ) :
(f + g).fin_meas_supp μ
theorem measure_theory.simple_func.fin_meas_supp.mul {α : Type u_1} {μ : measure_theory.measure α} {β : Type u_2} {f g : β} (hf : f.fin_meas_supp μ) (hg : g.fin_meas_supp μ) :
(f * g).fin_meas_supp μ
theorem measure_theory.simple_func.fin_meas_supp.lintegral_lt_top {α : Type u_1} {μ : measure_theory.measure α} (hm : f.fin_meas_supp μ) (hf : ∀ᵐ (a : α) ∂μ, f a < ) :
theorem measure_theory.simple_func.fin_meas_supp.iff_lintegral_lt_top {α : Type u_1} {μ : measure_theory.measure α} (hf : ∀ᵐ (a : α) ∂μ, f a < ) :
theorem measure_theory.simple_func.induction {α : Type u_1} {γ : Type u_2} [add_monoid γ] {P : → Prop} (h_ind : ∀ (c : γ) {s : set α} (hs : , ) (h_add : ∀ ⦃f g : ⦄, P fP gP (f + g)) (f : γ) :
P f

To prove something for an arbitrary simple function, it suffices to show that the property holds for (multiples of) characteristic functions and is closed under addition (of functions with disjoint support).

It is possible to make the hypotheses in `h_add` a bit stronger, and such conditions can be added once we need them (for example it is only necessary to consider the case where `g` is a multiple of a characteristic function, and that this multiple doesn't appear in the image of `f`)

def measure_theory.lintegral {α : Type u_1} (μ : measure_theory.measure α) (f : α → ℝ≥0∞) :

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} ⦃μ ν : measure_theory.measure α⦄ (hμν : μ ν) ⦃f g : α → ℝ≥0∞ (hfg : f g) :
∫⁻ (a : α), f a μ ∫⁻ (a : α), g a ν
theorem measure_theory.lintegral_mono {α : Type u_1} {μ : measure_theory.measure α} ⦃f g : α → ℝ≥0∞ (hfg : f g) :
∫⁻ (a : α), f a μ ∫⁻ (a : α), g a μ
theorem measure_theory.lintegral_mono_nnreal {α : Type u_1} {μ : measure_theory.measure α} {f g : α → ℝ≥0} (h : f g) :
∫⁻ (a : α), (f a) μ ∫⁻ (a : α), (g a) μ
theorem measure_theory.lintegral_mono_set {α : Type u_1} ⦃μ : measure_theory.measure α⦄ {s t : set α} {f : α → ℝ≥0∞} (hst : s t) :
∫⁻ (x : α) in s, f x μ ∫⁻ (x : α) in t, f x μ
theorem measure_theory.lintegral_mono_set' {α : Type u_1} ⦃μ : measure_theory.measure α⦄ {s t : set α} {f : α → ℝ≥0∞} (hst : s ≤ᵐ[μ] t) :
∫⁻ (x : α) in s, f x μ ∫⁻ (x : α) in t, f x μ
theorem measure_theory.monotone_lintegral {α : Type u_1} (μ : measure_theory.measure α) :
@[simp]
theorem measure_theory.lintegral_const {α : Type u_1} {μ : measure_theory.measure α} (c : ℝ≥0∞) :
∫⁻ (a : α), c μ = c *
@[simp]
theorem measure_theory.lintegral_one {α : Type u_1} {μ : measure_theory.measure α} :
∫⁻ (a : α), 1 μ =
theorem measure_theory.set_lintegral_const {α : Type u_1} {μ : measure_theory.measure α} (s : set α) (c : ℝ≥0∞) :
∫⁻ (a : α) in s, c μ = c * μ s
theorem measure_theory.set_lintegral_one {α : Type u_1} {μ : measure_theory.measure α} (s : set α) :
∫⁻ (a : α) in s, 1 μ = μ s
theorem measure_theory.lintegral_eq_nnreal {α : Type u_1} (f : α → ℝ≥0∞) (μ : 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} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} (h : ∫⁻ (x : α), f x μ < ) {ε : ℝ≥0∞} (hε : 0 < ε) :
∃ (φ : , (∀ (x : α), (φ x) f x) ∀ (ψ : , (∀ (x : α), (ψ x) f x) - φ)).lintegral μ < ε
theorem measure_theory.supr_lintegral_le {α : Type u_1} {μ : measure_theory.measure α} {ι : Sort u_2} (f : ι → α → ℝ≥0∞) :
(⨆ (i : ι), ∫⁻ (a : α), f i a μ) ∫⁻ (a : α), (⨆ (i : ι), f i a) μ
theorem measure_theory.supr2_lintegral_le {α : Type u_1} {μ : measure_theory.measure α} {ι : Sort u_2} {ι' : ι → Sort u_3} (f : Π (i : ι), ι' iα → ℝ≥0∞) :
(⨆ (i : ι) (h : ι' i), ∫⁻ (a : α), f i h a μ) ∫⁻ (a : α), (⨆ (i : ι) (h : ι' i), f i h a) μ
theorem measure_theory.le_infi_lintegral {α : Type u_1} {μ : measure_theory.measure α} {ι : Sort u_2} (f : ι → α → ℝ≥0∞) :
∫⁻ (a : α), (⨅ (i : ι), f i a) μ ⨅ (i : ι), ∫⁻ (a : α), f i a μ
theorem measure_theory.le_infi2_lintegral {α : Type u_1} {μ : measure_theory.measure α} {ι : Sort u_2} {ι' : ι → Sort u_3} (f : Π (i : ι), ι' iα → ℝ≥0∞) :
∫⁻ (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} {μ : measure_theory.measure α} {f g : α → ℝ≥0∞} (h : ∀ᵐ (a : α) ∂μ, f a g a) :
∫⁻ (a : α), f a μ ∫⁻ (a : α), g a μ
theorem measure_theory.lintegral_congr_ae {α : Type u_1} {μ : measure_theory.measure α} {f g : α → ℝ≥0∞} (h : f =ᵐ[μ] g) :
∫⁻ (a : α), f a μ = ∫⁻ (a : α), g a μ
theorem measure_theory.lintegral_congr {α : Type u_1} {μ : measure_theory.measure α} {f g : α → ℝ≥0∞} (h : ∀ (a : α), f a = g a) :
∫⁻ (a : α), f a μ = ∫⁻ (a : α), g a μ
theorem measure_theory.set_lintegral_congr {α : Type u_1} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} {s t : set α} (h : s =ᵐ[μ] t) :
∫⁻ (x : α) in s, f x μ = ∫⁻ (x : α) in t, f x μ
theorem measure_theory.lintegral_supr {α : Type u_1} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} (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} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} (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} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} {F : α → ℝ≥0∞} (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 (𝓝 (F x))) :
filter.tendsto (λ (n : ), ∫⁻ (x : α), f n x μ) filter.at_top (𝓝 (∫⁻ (x : α), F x μ))

Monotone convergence theorem expressed with limits

theorem measure_theory.lintegral_eq_supr_eapprox_lintegral {α : Type u_1} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} (hf : measurable f) :
∫⁻ (a : α), f a μ = ⨆ (n : ),
theorem measure_theory.exists_pos_set_lintegral_lt_of_measure_lt {α : Type u_1} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} (h : ∫⁻ (x : α), f x μ < ) {ε : ℝ≥0∞} (hε : 0 < ε) :
∃ (δ : ℝ≥0∞) (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} {μ : measure_theory.measure α} {ι : Type u_2} {f : α → ℝ≥0∞} (h : ∫⁻ (x : α), f x μ < ) {l : filter ι} {s : ι → set α} (hl : filter.tendsto (μ s) l (𝓝 0)) :
filter.tendsto (λ (i : ι), ∫⁻ (x : α) in s i, f x μ) l (𝓝 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.

@[simp]
theorem measure_theory.lintegral_add {α : Type u_1} {μ : measure_theory.measure α} {f g : α → ℝ≥0∞} (hf : measurable f) (hg : measurable g) :
∫⁻ (a : α), f a + g a μ = ∫⁻ (a : α), f a μ + ∫⁻ (a : α), g a μ
theorem measure_theory.lintegral_add' {α : Type u_1} {μ : measure_theory.measure α} {f g : α → ℝ≥0∞} (hf : μ) (hg : μ) :
∫⁻ (a : α), f a + g a μ = ∫⁻ (a : α), f a μ + ∫⁻ (a : α), g a μ
theorem measure_theory.lintegral_zero {α : Type u_1} {μ : measure_theory.measure α} :
∫⁻ (a : α), 0 μ = 0
theorem measure_theory.lintegral_zero_fun {α : Type u_1} {μ : measure_theory.measure α} :
∫⁻ (a : α), 0 a μ = 0
@[simp]
theorem measure_theory.lintegral_smul_measure {α : Type u_1} {μ : measure_theory.measure α} (c : ℝ≥0∞) (f : α → ℝ≥0∞) :
∫⁻ (a : α), f a c μ = c * ∫⁻ (a : α), f a μ
@[simp]
theorem measure_theory.lintegral_sum_measure {α : Type u_1} {ι : Type u_2} (f : α → ℝ≥0∞) (μ : ι → ) :
∫⁻ (a : α), f a = ∑' (i : ι), ∫⁻ (a : α), f a μ i
@[simp]
theorem measure_theory.lintegral_add_measure {α : Type u_1} (f : α → ℝ≥0∞) (μ ν : measure_theory.measure α) :
∫⁻ (a : α), f a + ν) = ∫⁻ (a : α), f a μ + ∫⁻ (a : α), f a ν
@[simp]
theorem measure_theory.lintegral_zero_measure {α : Type u_1} (f : α → ℝ≥0∞) :
∫⁻ (a : α), f a 0 = 0
theorem measure_theory.lintegral_finset_sum {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (s : finset β) {f : β → α → ℝ≥0∞} (hf : ∀ (b : β), b smeasurable (f b)) :
∫⁻ (a : α), ∑ (b : β) in s, f b a μ = ∑ (b : β) in s, ∫⁻ (a : α), f b a μ
@[simp]
theorem measure_theory.lintegral_const_mul {α : Type u_1} {μ : measure_theory.measure α} (r : ℝ≥0∞) {f : α → ℝ≥0∞} (hf : measurable f) :
∫⁻ (a : α), r * f a μ = r * ∫⁻ (a : α), f a μ
theorem measure_theory.lintegral_const_mul'' {α : Type u_1} {μ : measure_theory.measure α} (r : ℝ≥0∞) {f : α → ℝ≥0∞} (hf : μ) :
∫⁻ (a : α), r * f a μ = r * ∫⁻ (a : α), f a μ
theorem measure_theory.lintegral_const_mul_le {α : Type u_1} {μ : measure_theory.measure α} (r : ℝ≥0∞) (f : α → ℝ≥0∞) :
r * ∫⁻ (a : α), f a μ ∫⁻ (a : α), r * f a μ
theorem measure_theory.lintegral_const_mul' {α : Type u_1} {μ : measure_theory.measure α} (r : ℝ≥0∞) (f : α → ℝ≥0∞) (hr : r ) :
∫⁻ (a : α), r * f a μ = r * ∫⁻ (a : α), f a μ
theorem measure_theory.lintegral_mul_const {α : Type u_1} {μ : measure_theory.measure α} (r : ℝ≥0∞) {f : α → ℝ≥0∞} (hf : measurable f) :
∫⁻ (a : α), (f a) * r μ = (∫⁻ (a : α), f a μ) * r
theorem measure_theory.lintegral_mul_const'' {α : Type u_1} {μ : measure_theory.measure α} (r : ℝ≥0∞) {f : α → ℝ≥0∞} (hf : μ) :
∫⁻ (a : α), (f a) * r μ = (∫⁻ (a : α), f a μ) * r
theorem measure_theory.lintegral_mul_const_le {α : Type u_1} {μ : measure_theory.measure α} (r : ℝ≥0∞) (f : α → ℝ≥0∞) :
(∫⁻ (a : α), f a μ) * r ∫⁻ (a : α), (f a) * r μ
theorem measure_theory.lintegral_mul_const' {α : Type u_1} {μ : measure_theory.measure α} (r : ℝ≥0∞) (f : α → ℝ≥0∞) (hr : r ) :
∫⁻ (a : α), (f a) * r μ = (∫⁻ (a : α), f a μ) * r
theorem measure_theory.lintegral_lintegral_mul {α : Type u_1} {μ : measure_theory.measure α} {β : Type u_2} {ν : measure_theory.measure β} {f : α → ℝ≥0∞} {g : β → ℝ≥0∞} (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} {μ : measure_theory.measure α} {f f' : α → β} (h : f =ᵐ[μ] f') (g : β → ℝ≥0∞) :
∫⁻ (a : α), g (f a) μ = ∫⁻ (a : α), g (f' a) μ
theorem measure_theory.lintegral_rw₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μ : measure_theory.measure α} {f₁ f₁' : α → β} {f₂ f₂' : α → γ} (h₁ : f₁ =ᵐ[μ] f₁') (h₂ : f₂ =ᵐ[μ] f₂') (g : β → γ → ℝ≥0∞) :
∫⁻ (a : α), g (f₁ a) (f₂ a) μ = ∫⁻ (a : α), g (f₁' a) (f₂' a) μ
@[simp]
theorem measure_theory.lintegral_indicator {α : Type u_1} {μ : measure_theory.measure α} (f : α → ℝ≥0∞) {s : set α} (hs : measurable_set s) :
∫⁻ (a : α), s.indicator f a μ = ∫⁻ (a : α) in s, f a μ
theorem measure_theory.mul_meas_ge_le_lintegral {α : Type u_1} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} (hf : measurable f) (ε : ℝ≥0∞) :
ε * μ {x : α | ε f x} ∫⁻ (a : α), f a μ

Chebyshev's inequality

theorem measure_theory.meas_ge_le_lintegral_div {α : Type u_1} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} (hf : measurable f) {ε : ℝ≥0∞} (hε : ε 0) (hε' : ε ) :
μ {x : α | ε f x} ∫⁻ (a : α), f a μ / ε
@[simp]
theorem measure_theory.lintegral_eq_zero_iff {α : Type u_1} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} (hf : measurable f) :
∫⁻ (a : α), f a μ = 0 f =ᵐ[μ] 0
@[simp]
theorem measure_theory.lintegral_eq_zero_iff' {α : Type u_1} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} (hf : μ) :
∫⁻ (a : α), f a μ = 0 f =ᵐ[μ] 0
theorem measure_theory.lintegral_pos_iff_support {α : Type u_1} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} (hf : measurable f) :
0 < ∫⁻ (a : α), f a μ 0 < μ
theorem measure_theory.lintegral_supr_ae {α : Type u_1} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} (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} {μ : measure_theory.measure α} {f g : α → ℝ≥0∞} (hf : measurable f) (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_infi_ae {α : Type u_1} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} (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} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} (h_meas : ∀ (n : ), measurable (f n)) (h_mono : ∀ ⦃m n : ⦄, m nf n f m) (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} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} (h_meas : ∀ (n : ), ae_measurable (f n) μ) :
∫⁻ (a : α), filter.at_top.liminf (λ (n : ), f n a) μ filter.at_top.liminf (λ (n : ), ∫⁻ (a : α), f n a μ)

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

theorem measure_theory.lintegral_liminf_le {α : Type u_1} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} (h_meas : ∀ (n : ), measurable (f n)) :
∫⁻ (a : α), filter.at_top.liminf (λ (n : ), f n a) μ filter.at_top.liminf (λ (n : ), ∫⁻ (a : α), f n a μ)

Known as Fatou's lemma

theorem measure_theory.limsup_lintegral_le {α : Type u_1} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} {g : α → ℝ≥0∞} (hf_meas : ∀ (n : ), measurable (f n)) (h_bound : ∀ (n : ), f n ≤ᵐ[μ] g) (h_fin : ∫⁻ (a : α), g a μ < ) :
filter.at_top.limsup (λ (n : ), ∫⁻ (a : α), f n a μ) ∫⁻ (a : α), filter.at_top.limsup (λ (n : ), f n a) μ
theorem measure_theory.tendsto_lintegral_of_dominated_convergence {α : Type u_1} {μ : measure_theory.measure α} {F : α → ℝ≥0∞} {f : α → ℝ≥0∞} (bound : α → ℝ≥0∞) (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 (𝓝 (f a))) :
filter.tendsto (λ (n : ), ∫⁻ (a : α), F n a μ) filter.at_top (𝓝 (∫⁻ (a : α), f a μ))

Dominated convergence theorem for nonnegative functions

theorem measure_theory.tendsto_lintegral_of_dominated_convergence' {α : Type u_1} {μ : measure_theory.measure α} {F : α → ℝ≥0∞} {f : α → ℝ≥0∞} (bound : α → ℝ≥0∞) (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 (𝓝 (f a))) :
filter.tendsto (λ (n : ), ∫⁻ (a : α), F n a μ) filter.at_top (𝓝 (∫⁻ (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} {μ : measure_theory.measure α} {ι : Type u_2} {l : filter ι} {F : ι → α → ℝ≥0∞} {f : α → ℝ≥0∞} (bound : α → ℝ≥0∞) (hl_cb : l.is_countably_generated) (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 (𝓝 (f a))) :
filter.tendsto (λ (n : ι), ∫⁻ (a : α), F n a μ) l (𝓝 (∫⁻ (a : α), f a μ))

Dominated convergence theorem for filters with a countable basis

theorem measure_theory.lintegral_supr_directed {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [encodable β] {f : β → α → ℝ≥0∞} (hf : ∀ (b : β), measurable (f b)) (h_directed : f) :
∫⁻ (a : α), (⨆ (b : β), f b a) μ = ⨆ (b : β), ∫⁻ (a : α), f b a μ

Monotone convergence for a suprema over a directed family and indexed by an encodable type

theorem measure_theory.lintegral_tsum {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [encodable β] {f : β → α → ℝ≥0∞} (hf : ∀ (i : β), measurable (f i)) :
∫⁻ (a : α), ∑' (i : β), f i a μ = ∑' (i : β), ∫⁻ (a : α), f i a μ
theorem measure_theory.lintegral_Union {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [encodable β] {s : β → set α} (hm : ∀ (i : β), measurable_set (s i)) (hd : pairwise (disjoint on s)) (f : α → ℝ≥0∞) :
∫⁻ (a : α) in ⋃ (i : β), s i, f a μ = ∑' (i : β), ∫⁻ (a : α) in s i, f a μ
theorem measure_theory.lintegral_Union_le {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [encodable β] (s : β → set α) (f : α → ℝ≥0∞) :
∫⁻ (a : α) in ⋃ (i : β), s i, f a μ ∑' (i : β), ∫⁻ (a : α) in s i, f a μ
theorem measure_theory.lintegral_union {α : Type u_1} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} {A B : set α} (hA : measurable_set A) (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_map {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {f : β → ℝ≥0∞} {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} {μ : measure_theory.measure α} {f : β → ℝ≥0∞} {g : α → β} (hf : μ)) (hg : measurable g) :
∫⁻ (a : β), f a = ∫⁻ (a : α), f (g a) μ
theorem measure_theory.lintegral_comp {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {f : β → ℝ≥0∞} {g : α → β} (hf : measurable f) (hg : measurable g) :
(f g) = ∫⁻ (a : β), f a
theorem measure_theory.set_lintegral_map {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {f : β → ℝ≥0∞} {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_map_equiv {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f : β → ℝ≥0∞) (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.lintegral_dirac' {α : Type u_1} (a : α) {f : α → ℝ≥0∞} (hf : measurable f) :
∫⁻ (a : α), f a = f a
theorem measure_theory.lintegral_dirac {α : Type u_1} (a : α) (f : α → ℝ≥0∞) :
∫⁻ (a : α), f a = f a
theorem measure_theory.lintegral_count' {α : Type u_1} {f : α → ℝ≥0∞} (hf : measurable f) :
∫⁻ (a : α), f a measure_theory.measure.count = ∑' (a : α), f a
theorem measure_theory.lintegral_count {α : Type u_1} (f : α → ℝ≥0∞) :
∫⁻ (a : α), f a measure_theory.measure.count = ∑' (a : α), f a
theorem measure_theory.ae_lt_top {α : Type u_1} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} (hf : measurable f) (h2f : ∫⁻ (x : α), f x μ < ) :
∀ᵐ (x : α) ∂μ, f x <
theorem measure_theory.ae_lt_top' {α : Type u_1} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} (hf : μ) (h2f : ∫⁻ (x : α), f x μ < ) :
∀ᵐ (x : α) ∂μ, f x <
def measure_theory.measure.with_density {α : Type u_1} (μ : measure_theory.measure α) (f : α → ℝ≥0∞) :

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
@[simp]
theorem measure_theory.with_density_apply {α : Type u_1} {μ : measure_theory.measure α} (f : α → ℝ≥0∞) {s : set α} (hs : measurable_set s) :
(μ.with_density f) s = ∫⁻ (a : α) in s, f a μ
theorem measurable.ennreal_induction {α : Type u_1} {P : (α → ℝ≥0∞) → Prop} (h_ind : ∀ (c : ℝ≥0∞) ⦃s : set α⦄, P (s.indicator (λ (_x : α), c))) (h_add : ∀ ⦃f g : α → ℝ≥0∞⦄, P fP gP (f + g)) (h_supr : ∀ ⦃f : α → ℝ≥0∞⦄, (∀ (n : ), measurable (f n))(∀ (n : ), P (f n))P (λ (x : α), ⨆ (n : ), f n x)) ⦃f : α → ℝ≥0∞ (hf : measurable f) :
P f

To prove something for an arbitrary measurable function into `ℝ≥0∞`, it suffices to show that the property holds for (multiples of) characteristic functions and is closed under addition and supremum of increasing sequences of functions.

It is possible to make the hypotheses in the induction steps a bit stronger, and such conditions can be added once we need them (for example in `h_add` it is only necessary to consider the sum of a simple function with a multiple of a characteristic function and that the intersection of their images is a subset of `{0}`.

theorem measure_theory.lintegral_with_density_eq_lintegral_mul {α : Type u_1} (μ : measure_theory.measure α) {f : α → ℝ≥0∞} (h_mf : measurable f) {g : α → ℝ≥0∞} :
∫⁻ (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.exists_integrable_pos_of_sigma_finite {α : Type u_1} (μ : measure_theory.measure α) {ε : ℝ≥0} (εpos : 0 < ε) :
∃ (g : α → ℝ≥0), (∀ (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 : α → ℝ≥0∞} (hf : measurable f) :
measure_theory.lintegral (μ.trim hm) f = ∫⁻ (a : α), f a μ
theorem measure_theory.lintegral_trim_ae {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) {f : α → ℝ≥0∞} (hf : (μ.trim hm)) :
measure_theory.lintegral (μ.trim hm) f = ∫⁻ (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 : ℝ≥0∞) {f : set αℝ≥0∞} (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 : ℝ≥0∞) {f : α → ℝ≥0∞} (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 : ℝ≥0∞) {f : α → ℝ≥0∞} (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 : ℝ≥0∞) {f : α → ℝ≥0∞} (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.