mathlib documentation

measure_theory.integral.lebesgue

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

source
structure measure_theory.simple_func (α : Type u) [measurable_space α] (β : 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.

Instances for measure_theory.simple_func
source
@[protected, instance]
def measure_theory.simple_func.has_coe_to_fun {α : Type u_1} {β : Type u_2} [measurable_space α] :
has_coe_to_fun (measure_theory.simple_func α β) (λ (_x : measure_theory.simple_func α β), α → β)
Equations
source
theorem measure_theory.simple_func.coe_injective {α : Type u_1} {β : Type u_2} [measurable_space α] ⦃f g : measure_theory.simple_func α β⦄ (H : ⇑f = ⇑g) :
f = g
source
@[ext]
theorem measure_theory.simple_func.ext {α : Type u_1} {β : Type u_2} [measurable_space α] {f g : measure_theory.simple_func α β} (H : ∀ (a : α), ⇑f a = ⇑g a) :
f = g
source
theorem measure_theory.simple_func.finite_range {α : Type u_1} {β : Type u_2} [measurable_space α] (f : measure_theory.simple_func α β) :
(set.range ⇑f).finite
source
theorem measure_theory.simple_func.measurable_set_fiber {α : Type u_1} {β : Type u_2} [measurable_space α] (f : measure_theory.simple_func α β) (x : β) :
measurable_set (⇑f ⁻¹' {x})
source
@[simp]
theorem measure_theory.simple_func.apply_mk {α : Type u_1} {β : Type u_2} [measurable_space α] (f : α → β) (h : ∀ (x : β), measurable_set (f ⁻¹' {x})) (h' : (set.range f).finite) (x : α) :
⇑{to_fun := f, measurable_set_fiber' := h, finite_range' := h'} x = f x
source
def measure_theory.simple_func.of_is_empty {α : Type u_1} {β : Type u_2} [measurable_space α] [is_empty α] :
measure_theory.simple_func α β

Simple function defined on the empty type.

Equations
source
@[protected]
noncomputable def measure_theory.simple_func.range {α : Type u_1} {β : Type u_2} [measurable_space α] (f : measure_theory.simple_func α β) :
finset β

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

Equations
source
@[simp]
theorem measure_theory.simple_func.mem_range {α : Type u_1} {β : Type u_2} [measurable_space α] {f : measure_theory.simple_func α β} {b : β} :
b ∈ f.range ↔ b ∈ set.range ⇑f
source
theorem measure_theory.simple_func.mem_range_self {α : Type u_1} {β : Type u_2} [measurable_space α] (f : measure_theory.simple_func α β) (x : α) :
⇑f x ∈ f.range
source
@[simp]
theorem measure_theory.simple_func.coe_range {α : Type u_1} {β : Type u_2} [measurable_space α] (f : measure_theory.simple_func α β) :
↑(f.range) = set.range ⇑f
source
theorem measure_theory.simple_func.mem_range_of_measure_ne_zero {α : Type u_1} {β : Type u_2} [measurable_space α] {f : measure_theory.simple_func α β} {x : β} {μ : measure_theory.measure α} (H : ⇑μ (⇑f ⁻¹' {x}) ≠ 0) :
x ∈ f.range
source
theorem measure_theory.simple_func.forall_range_iff {α : Type u_1} {β : Type u_2} [measurable_space α] {f : measure_theory.simple_func α β} {p : β → Prop} :
(∀ (y : β), y ∈ f.range → p y) ↔ ∀ (x : α), p (⇑f x)
source
theorem measure_theory.simple_func.exists_range_iff {α : Type u_1} {β : Type u_2} [measurable_space α] {f : measure_theory.simple_func α β} {p : β → Prop} :
(∃ (y : β) (H : y ∈ f.range), p y) ↔ ∃ (x : α), p (⇑f x)
source
theorem measure_theory.simple_func.preimage_eq_empty_iff {α : Type u_1} {β : Type u_2} [measurable_space α] (f : measure_theory.simple_func α β) (b : β) :
⇑f ⁻¹' {b} = ∅ ↔ b ∉ f.range
source
theorem measure_theory.simple_func.exists_forall_le {α : Type u_1} {β : Type u_2} [measurable_space α] [nonempty β] [preorder β] [is_directed β has_le.le] (f : measure_theory.simple_func α β) :
∃ (C : β), ∀ (x : α), ⇑f x ≤ C
source
def measure_theory.simple_func.const (α : Type u_1) {β : Type u_2} [measurable_space α] (b : β) :
measure_theory.simple_func α β

Constant function as a simple_func.

Equations
source
@[protected, instance]
def measure_theory.simple_func.inhabited {α : Type u_1} {β : Type u_2} [measurable_space α] [inhabited β] :
inhabited (measure_theory.simple_func α β)
Equations
source
theorem measure_theory.simple_func.const_apply {α : Type u_1} {β : Type u_2} [measurable_space α] (a : α) (b : β) :
⇑(measure_theory.simple_func.const α b) a = b
source
@[simp]
theorem measure_theory.simple_func.coe_const {α : Type u_1} {β : Type u_2} [measurable_space α] (b : β) :
⇑(measure_theory.simple_func.const α b) = function.const α b
source
@[simp]
theorem measure_theory.simple_func.range_const {β : Type u_2} (α : Type u_1) [measurable_space α] [nonempty α] (b : β) :
(measure_theory.simple_func.const α b).range = {b}
source
theorem measure_theory.simple_func.range_const_subset {β : Type u_2} (α : Type u_1) [measurable_space α] (b : β) :
(measure_theory.simple_func.const α b).range ⊆ {b}
source
theorem measure_theory.simple_func.simple_func_bot {β : Type u_2} {α : Type u_1} (f : measure_theory.simple_func α β) [nonempty β] :
∃ (c : β), ∀ (x : α), ⇑f x = c
source
theorem measure_theory.simple_func.simple_func_bot' {β : Type u_2} {α : Type u_1} [nonempty β] (f : measure_theory.simple_func α β) :
∃ (c : β), f = measure_theory.simple_func.const α c
source
theorem measure_theory.simple_func.measurable_set_cut {α : Type u_1} {β : Type u_2} [measurable_space α] (r : α → β → Prop) (f : measure_theory.simple_func α β) (h : ∀ (b : β), measurable_set {a : α | r a b}) :
measurable_set {a : α | r a (⇑f a)}
source
@[measurability]
theorem measure_theory.simple_func.measurable_set_preimage {α : Type u_1} {β : Type u_2} [measurable_space α] (f : measure_theory.simple_func α β) (s : set β) :
measurable_set (⇑f ⁻¹' s)
source
@[protected, measurability]
theorem measure_theory.simple_func.measurable {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] (f : measure_theory.simple_func α β) :
measurable ⇑f

A simple function is measurable

source
@[protected, measurability]
theorem measure_theory.simple_func.ae_measurable {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} (f : measure_theory.simple_func α β) :
ae_measurable ⇑f μ
source
@[protected]
theorem measure_theory.simple_func.sum_measure_preimage_singleton {α : Type u_1} {β : Type u_2} [measurable_space α] (f : measure_theory.simple_func α β) {μ : measure_theory.measure α} (s : finset β) :
s.sum (λ (y : β), ⇑μ (⇑f ⁻¹' {y})) = ⇑μ (⇑f ⁻¹' ↑s)
source
theorem measure_theory.simple_func.sum_range_measure_preimage_singleton {α : Type u_1} {β : Type u_2} [measurable_space α] (f : measure_theory.simple_func α β) (μ : measure_theory.measure α) :
f.range.sum (λ (y : β), ⇑μ (⇑f ⁻¹' {y})) = ⇑μ set.univ
source
noncomputable def measure_theory.simple_func.piecewise {α : Type u_1} {β : Type u_2} [measurable_space α] (s : set α) (hs : measurable_set s) (f g : measure_theory.simple_func α β) :
measure_theory.simple_func α β

If-then-else as a simple_func.

Equations
source
@[simp]
theorem measure_theory.simple_func.coe_piecewise {α : Type u_1} {β : Type u_2} [measurable_space α] {s : set α} (hs : measurable_set s) (f g : measure_theory.simple_func α β) :
⇑(measure_theory.simple_func.piecewise s hs f g) = s.piecewise ⇑f ⇑g
source
theorem measure_theory.simple_func.piecewise_apply {α : Type u_1} {β : Type u_2} [measurable_space α] {s : set α} (hs : measurable_set s) (f g : measure_theory.simple_func α β) (a : α) :
⇑(measure_theory.simple_func.piecewise s hs f g) a = ite (a ∈ s) (⇑f a) (⇑g a)
source
@[simp]
theorem measure_theory.simple_func.piecewise_compl {α : Type u_1} {β : Type u_2} [measurable_space α] {s : set α} (hs : measurable_set sᶜ) (f g : measure_theory.simple_func α β) :
measure_theory.simple_func.piecewise sᶜ hs f g = measure_theory.simple_func.piecewise s _ g f
source
@[simp]
theorem measure_theory.simple_func.piecewise_univ {α : Type u_1} {β : Type u_2} [measurable_space α] (f g : measure_theory.simple_func α β) :
measure_theory.simple_func.piecewise set.univ measurable_set.univ f g = f
source
@[simp]
theorem measure_theory.simple_func.piecewise_empty {α : Type u_1} {β : Type u_2} [measurable_space α] (f g : measure_theory.simple_func α β) :
measure_theory.simple_func.piecewise ∅ measurable_set.empty f g = g
source
theorem measure_theory.simple_func.support_indicator {α : Type u_1} {β : Type u_2} [measurable_space α] [has_zero β] {s : set α} (hs : measurable_set s) (f : measure_theory.simple_func α β) :
function.support ⇑(measure_theory.simple_func.piecewise s hs f (measure_theory.simple_func.const α 0)) = s ∩ function.support ⇑f
source
theorem measure_theory.simple_func.range_indicator {α : Type u_1} {β : Type u_2} [measurable_space α] {s : set α} (hs : measurable_set s) (hs_nonempty : s.nonempty) (hs_ne_univ : s ≠ set.univ) (x y : β) :
(measure_theory.simple_func.piecewise s hs (measure_theory.simple_func.const α x) (measure_theory.simple_func.const α y)).range = {x, y}
source
theorem measure_theory.simple_func.measurable_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space γ] (f : measure_theory.simple_func α β) (g : β → α → γ) (hg : ∀ (b : β), measurable (g b)) :
measurable (λ (a : α), g (⇑f a) a)
source
def measure_theory.simple_func.bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] (f : measure_theory.simple_func α β) (g : β → measure_theory.simple_func α γ) :
measure_theory.simple_func α γ

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
source
@[simp]
theorem measure_theory.simple_func.bind_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] (f : measure_theory.simple_func α β) (g : β → measure_theory.simple_func α γ) (a : α) :
⇑(f.bind g) a = ⇑(g (⇑f a)) a
source
def measure_theory.simple_func.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] (g : β → γ) (f : measure_theory.simple_func α β) :
measure_theory.simple_func α γ

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

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

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

Equations
source
@[simp]
theorem measure_theory.simple_func.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] (f : measure_theory.simple_func β γ) {g : α → β} (hgm : measurable g) :
⇑(f.comp g hgm) = ⇑f ∘ g
source
theorem measure_theory.simple_func.range_comp_subset_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] (f : measure_theory.simple_func β γ) {g : α → β} (hgm : measurable g) :
(f.comp g hgm).range ⊆ f.range
source
noncomputable def measure_theory.simple_func.extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] (f₁ : measure_theory.simple_func α γ) (g : α → β) (hg : measurable_embedding g) (f₂ : measure_theory.simple_func β γ) :
measure_theory.simple_func β γ

Extend a simple_func along a measurable embedding: f₁.extend g hg f₂ is the function F : β →ₛ γ such that F ∘ g = f₁ and F y = f₂ y whenever y ∉ range g.

Equations
source
@[simp]
theorem measure_theory.simple_func.extend_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] (f₁ : measure_theory.simple_func α γ) {g : α → β} (hg : measurable_embedding g) (f₂ : measure_theory.simple_func β γ) (x : α) :
⇑(f₁.extend g hg f₂) (g x) = ⇑f₁ x
source
@[simp]
theorem measure_theory.simple_func.extend_apply' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] (f₁ : measure_theory.simple_func α γ) {g : α → β} (hg : measurable_embedding g) (f₂ : measure_theory.simple_func β γ) {y : β} (h : ¬∃ (x : α), g x = y) :
⇑(f₁.extend g hg f₂) y = ⇑f₂ y
source
@[simp]
theorem measure_theory.simple_func.extend_comp_eq' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] (f₁ : measure_theory.simple_func α γ) {g : α → β} (hg : measurable_embedding g) (f₂ : measure_theory.simple_func β γ) :
⇑(f₁.extend g hg f₂) ∘ g = ⇑f₁
source
@[simp]
theorem measure_theory.simple_func.extend_comp_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] (f₁ : measure_theory.simple_func α γ) {g : α → β} (hg : measurable_embedding g) (f₂ : measure_theory.simple_func β γ) :
(f₁.extend g hg f₂).comp g _ = f₁
source
def measure_theory.simple_func.seq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] (f : measure_theory.simple_func α (β → γ)) (g : measure_theory.simple_func α β) :
measure_theory.simple_func α γ

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
source
@[simp]
theorem measure_theory.simple_func.seq_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] (f : measure_theory.simple_func α (β → γ)) (g : measure_theory.simple_func α β) (a : α) :
⇑(f.seq g) a = ⇑f a (⇑g a)
source
def measure_theory.simple_func.pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] (f : measure_theory.simple_func α β) (g : measure_theory.simple_func α γ) :
measure_theory.simple_func α (β × γ)

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

Equations
source
@[simp]
theorem measure_theory.simple_func.pair_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] (f : measure_theory.simple_func α β) (g : measure_theory.simple_func α γ) (a : α) :
⇑(f.pair g) a = (⇑f a, ⇑g a)
source
theorem measure_theory.simple_func.pair_preimage {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] (f : measure_theory.simple_func α β) (g : measure_theory.simple_func α γ) (s : set β) (t : set γ) :
⇑(f.pair g) ⁻¹' s ×ˢ t = ⇑f ⁻¹' s ∩ ⇑g ⁻¹' t
source
theorem measure_theory.simple_func.pair_preimage_singleton {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] (f : measure_theory.simple_func α β) (g : measure_theory.simple_func α γ) (b : β) (c : γ) :
⇑(f.pair g) ⁻¹' {(b, c)} = ⇑f ⁻¹' {b} ∩ ⇑g ⁻¹' {c}
source
theorem measure_theory.simple_func.bind_const {α : Type u_1} {β : Type u_2} [measurable_space α] (f : measure_theory.simple_func α β) :
f.bind (measure_theory.simple_func.const α) = f
source
@[protected, instance]
def measure_theory.simple_func.has_zero {α : Type u_1} {β : Type u_2} [measurable_space α] [has_zero β] :
has_zero (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.has_one {α : Type u_1} {β : Type u_2} [measurable_space α] [has_one β] :
has_one (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.has_add {α : Type u_1} {β : Type u_2} [measurable_space α] [has_add β] :
has_add (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.has_mul {α : Type u_1} {β : Type u_2} [measurable_space α] [has_mul β] :
has_mul (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.has_div {α : Type u_1} {β : Type u_2} [measurable_space α] [has_div β] :
has_div (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.has_sub {α : Type u_1} {β : Type u_2} [measurable_space α] [has_sub β] :
has_sub (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.has_inv {α : Type u_1} {β : Type u_2} [measurable_space α] [has_inv β] :
has_inv (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.has_neg {α : Type u_1} {β : Type u_2} [measurable_space α] [has_neg β] :
has_neg (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.has_sup {α : Type u_1} {β : Type u_2} [measurable_space α] [has_sup β] :
has_sup (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.has_inf {α : Type u_1} {β : Type u_2} [measurable_space α] [has_inf β] :
has_inf (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.has_le {α : Type u_1} {β : Type u_2} [measurable_space α] [has_le β] :
has_le (measure_theory.simple_func α β)
Equations
source
@[simp]
theorem measure_theory.simple_func.const_one {α : Type u_1} {β : Type u_2} [measurable_space α] [has_one β] :
measure_theory.simple_func.const α 1 = 1
source
@[simp]
theorem measure_theory.simple_func.const_zero {α : Type u_1} {β : Type u_2} [measurable_space α] [has_zero β] :
measure_theory.simple_func.const α 0 = 0
source
@[simp, norm_cast]
theorem measure_theory.simple_func.coe_one {α : Type u_1} {β : Type u_2} [measurable_space α] [has_one β] :
⇑1 = 1
source
@[simp, norm_cast]
theorem measure_theory.simple_func.coe_zero {α : Type u_1} {β : Type u_2} [measurable_space α] [has_zero β] :
⇑0 = 0
source
@[simp, norm_cast]
theorem measure_theory.simple_func.coe_mul {α : Type u_1} {β : Type u_2} [measurable_space α] [has_mul β] (f g : measure_theory.simple_func α β) :
⇑(f * g) = ⇑f * ⇑g
source
@[simp, norm_cast]
theorem measure_theory.simple_func.coe_add {α : Type u_1} {β : Type u_2} [measurable_space α] [has_add β] (f g : measure_theory.simple_func α β) :
⇑(f + g) = ⇑f + ⇑g
source
@[simp, norm_cast]
theorem measure_theory.simple_func.coe_inv {α : Type u_1} {β : Type u_2} [measurable_space α] [has_inv β] (f : measure_theory.simple_func α β) :
⇑f⁻¹ = (⇑f)⁻¹
source
@[simp, norm_cast]
theorem measure_theory.simple_func.coe_neg {α : Type u_1} {β : Type u_2} [measurable_space α] [has_neg β] (f : measure_theory.simple_func α β) :
⇑-f = -⇑f
source
@[simp, norm_cast]
theorem measure_theory.simple_func.coe_div {α : Type u_1} {β : Type u_2} [measurable_space α] [has_div β] (f g : measure_theory.simple_func α β) :
⇑(f / g) = ⇑f / ⇑g
source
@[simp, norm_cast]
theorem measure_theory.simple_func.coe_sub {α : Type u_1} {β : Type u_2} [measurable_space α] [has_sub β] (f g : measure_theory.simple_func α β) :
⇑(f - g) = ⇑f - ⇑g
source
@[simp, norm_cast]
theorem measure_theory.simple_func.coe_le {α : Type u_1} {β : Type u_2} [measurable_space α] [preorder β] {f g : measure_theory.simple_func α β} :
⇑f ≤ ⇑g ↔ f ≤ g
source
@[simp, norm_cast]
theorem measure_theory.simple_func.coe_sup {α : Type u_1} {β : Type u_2} [measurable_space α] [has_sup β] (f g : measure_theory.simple_func α β) :
⇑(f ⊔ g) = ⇑f ⊔ ⇑g
source
@[simp, norm_cast]
theorem measure_theory.simple_func.coe_inf {α : Type u_1} {β : Type u_2} [measurable_space α] [has_inf β] (f g : measure_theory.simple_func α β) :
⇑(f ⊓ g) = ⇑f ⊓ ⇑g
source
theorem measure_theory.simple_func.add_apply {α : Type u_1} {β : Type u_2} [measurable_space α] [has_add β] (f g : measure_theory.simple_func α β) (a : α) :
⇑(f + g) a = ⇑f a + ⇑g a
source
theorem measure_theory.simple_func.mul_apply {α : Type u_1} {β : Type u_2} [measurable_space α] [has_mul β] (f g : measure_theory.simple_func α β) (a : α) :
⇑(f * g) a = ⇑f a * ⇑g a
source
theorem measure_theory.simple_func.div_apply {α : Type u_1} {β : Type u_2} [measurable_space α] [has_div β] (f g : measure_theory.simple_func α β) (x : α) :
⇑(f / g) x = ⇑f x / ⇑g x
source
theorem measure_theory.simple_func.sub_apply {α : Type u_1} {β : Type u_2} [measurable_space α] [has_sub β] (f g : measure_theory.simple_func α β) (x : α) :
⇑(f - g) x = ⇑f x - ⇑g x
source
theorem measure_theory.simple_func.neg_apply {α : Type u_1} {β : Type u_2} [measurable_space α] [has_neg β] (f : measure_theory.simple_func α β) (x : α) :
(⇑-f) x = -⇑f x
source
theorem measure_theory.simple_func.inv_apply {α : Type u_1} {β : Type u_2} [measurable_space α] [has_inv β] (f : measure_theory.simple_func α β) (x : α) :
⇑f⁻¹ x = (⇑f x)⁻¹
source
theorem measure_theory.simple_func.sup_apply {α : Type u_1} {β : Type u_2} [measurable_space α] [has_sup β] (f g : measure_theory.simple_func α β) (a : α) :
⇑(f ⊔ g) a = ⇑f a ⊔ ⇑g a
source
theorem measure_theory.simple_func.inf_apply {α : Type u_1} {β : Type u_2} [measurable_space α] [has_inf β] (f g : measure_theory.simple_func α β) (a : α) :
⇑(f ⊓ g) a = ⇑f a ⊓ ⇑g a
source
@[simp]
theorem measure_theory.simple_func.range_one {α : Type u_1} {β : Type u_2} [measurable_space α] [nonempty α] [has_one β] :
1.range = {1}
source
@[simp]
theorem measure_theory.simple_func.range_zero {α : Type u_1} {β : Type u_2} [measurable_space α] [nonempty α] [has_zero β] :
0.range = {0}
source
@[simp]
theorem measure_theory.simple_func.range_eq_empty_of_is_empty {α : Type u_1} [measurable_space α] {β : Type u_2} [hα : is_empty α] (f : measure_theory.simple_func α β) :
f.range = ∅
source
theorem measure_theory.simple_func.eq_zero_of_mem_range_zero {α : Type u_1} {β : Type u_2} [measurable_space α] [has_zero β] {y : β} :
y ∈ 0.range → y = 0
source
theorem measure_theory.simple_func.add_eq_map₂ {α : Type u_1} {β : Type u_2} [measurable_space α] [has_add β] (f g : measure_theory.simple_func α β) :
f + g = measure_theory.simple_func.map (λ (p : β × β), p.fst + p.snd) (f.pair g)
source
theorem measure_theory.simple_func.mul_eq_map₂ {α : Type u_1} {β : Type u_2} [measurable_space α] [has_mul β] (f g : measure_theory.simple_func α β) :
f * g = measure_theory.simple_func.map (λ (p : β × β), p.fst * p.snd) (f.pair g)
source
theorem measure_theory.simple_func.sup_eq_map₂ {α : Type u_1} {β : Type u_2} [measurable_space α] [has_sup β] (f g : measure_theory.simple_func α β) :
f ⊔ g = measure_theory.simple_func.map (λ (p : β × β), p.fst ⊔ p.snd) (f.pair g)
source
theorem measure_theory.simple_func.const_mul_eq_map {α : Type u_1} {β : Type u_2} [measurable_space α] [has_mul β] (f : measure_theory.simple_func α β) (b : β) :
measure_theory.simple_func.const α b * f = measure_theory.simple_func.map (λ (a : β), b * a) f
source
theorem measure_theory.simple_func.const_add_eq_map {α : Type u_1} {β : Type u_2} [measurable_space α] [has_add β] (f : measure_theory.simple_func α β) (b : β) :
measure_theory.simple_func.const α b + f = measure_theory.simple_func.map (λ (a : β), b + a) f
source
theorem measure_theory.simple_func.map_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [has_add β] [has_add γ] {g : β → γ} (hg : ∀ (x y : β), g (x + y) = g x + g y) (f₁ f₂ : measure_theory.simple_func α β) :
measure_theory.simple_func.map g (f₁ + f₂) = measure_theory.simple_func.map g f₁ + measure_theory.simple_func.map g f₂
source
theorem measure_theory.simple_func.map_mul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [has_mul β] [has_mul γ] {g : β → γ} (hg : ∀ (x y : β), g (x * y) = g x * g y) (f₁ f₂ : measure_theory.simple_func α β) :
measure_theory.simple_func.map g (f₁ * f₂) = measure_theory.simple_func.map g f₁ * measure_theory.simple_func.map g f₂
source
@[protected, instance]
def measure_theory.simple_func.has_smul {α : Type u_1} {β : Type u_2} [measurable_space α] {K : Type u_5} [has_smul K β] :
has_smul K (measure_theory.simple_func α β)
Equations
source
@[simp]
theorem measure_theory.simple_func.coe_smul {α : Type u_1} {β : Type u_2} [measurable_space α] {K : Type u_5} [has_smul K β] (c : K) (f : measure_theory.simple_func α β) :
⇑(c • f) = c • ⇑f
source
theorem measure_theory.simple_func.smul_apply {α : Type u_1} {β : Type u_2} [measurable_space α] {K : Type u_5} [has_smul K β] (k : K) (f : measure_theory.simple_func α β) (a : α) :
⇑(k • f) a = k • ⇑f a
source
@[protected, instance]
def measure_theory.simple_func.has_nat_pow {α : Type u_1} {β : Type u_2} [measurable_space α] [monoid β] :
has_pow (measure_theory.simple_func α β) ℕ
Equations
source
@[simp]
theorem measure_theory.simple_func.coe_pow {α : Type u_1} {β : Type u_2} [measurable_space α] [monoid β] (f : measure_theory.simple_func α β) (n : ℕ) :
⇑(f ^ n) = ⇑f ^ n
source
theorem measure_theory.simple_func.pow_apply {α : Type u_1} {β : Type u_2} [measurable_space α] [monoid β] (n : ℕ) (f : measure_theory.simple_func α β) (a : α) :
⇑(f ^ n) a = ⇑f a ^ n
source
@[protected, instance]
def measure_theory.simple_func.has_int_pow {α : Type u_1} {β : Type u_2} [measurable_space α] [div_inv_monoid β] :
has_pow (measure_theory.simple_func α β) ℤ
Equations
source
@[simp]
theorem measure_theory.simple_func.coe_zpow {α : Type u_1} {β : Type u_2} [measurable_space α] [div_inv_monoid β] (f : measure_theory.simple_func α β) (z : ℤ) :
⇑(f ^ z) = ⇑f ^ z
source
theorem measure_theory.simple_func.zpow_apply {α : Type u_1} {β : Type u_2} [measurable_space α] [div_inv_monoid β] (z : ℤ) (f : measure_theory.simple_func α β) (a : α) :
⇑(f ^ z) a = ⇑f a ^ z
source
@[protected, instance]
def measure_theory.simple_func.add_monoid {α : Type u_1} {β : Type u_2} [measurable_space α] [add_monoid β] :
add_monoid (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.add_comm_monoid {α : Type u_1} {β : Type u_2} [measurable_space α] [add_comm_monoid β] :
add_comm_monoid (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.add_group {α : Type u_1} {β : Type u_2} [measurable_space α] [add_group β] :
add_group (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.add_comm_group {α : Type u_1} {β : Type u_2} [measurable_space α] [add_comm_group β] :
add_comm_group (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.monoid {α : Type u_1} {β : Type u_2} [measurable_space α] [monoid β] :
monoid (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.comm_monoid {α : Type u_1} {β : Type u_2} [measurable_space α] [comm_monoid β] :
comm_monoid (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.group {α : Type u_1} {β : Type u_2} [measurable_space α] [group β] :
group (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.comm_group {α : Type u_1} {β : Type u_2} [measurable_space α] [comm_group β] :
comm_group (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.module {α : Type u_1} {β : Type u_2} [measurable_space α] {K : Type u_5} [semiring K] [add_comm_monoid β] [module K β] :
module K (measure_theory.simple_func α β)
Equations
source
theorem measure_theory.simple_func.smul_eq_map {α : Type u_1} {β : Type u_2} [measurable_space α] {K : Type u_5} [has_smul K β] (k : K) (f : measure_theory.simple_func α β) :
k • f = measure_theory.simple_func.map (has_smul.smul k) f
source
@[protected, instance]
def measure_theory.simple_func.preorder {α : Type u_1} {β : Type u_2} [measurable_space α] [preorder β] :
preorder (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.partial_order {α : Type u_1} {β : Type u_2} [measurable_space α] [partial_order β] :
partial_order (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.order_bot {α : Type u_1} {β : Type u_2} [measurable_space α] [has_le β] [order_bot β] :
order_bot (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.order_top {α : Type u_1} {β : Type u_2} [measurable_space α] [has_le β] [order_top β] :
order_top (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.semilattice_inf {α : Type u_1} {β : Type u_2} [measurable_space α] [semilattice_inf β] :
semilattice_inf (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.semilattice_sup {α : Type u_1} {β : Type u_2} [measurable_space α] [semilattice_sup β] :
semilattice_sup (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.lattice {α : Type u_1} {β : Type u_2} [measurable_space α] [lattice β] :
lattice (measure_theory.simple_func α β)
Equations
source
@[protected, instance]
def measure_theory.simple_func.bounded_order {α : Type u_1} {β : Type u_2} [measurable_space α] [has_le β] [bounded_order β] :
bounded_order (measure_theory.simple_func α β)
Equations
source
theorem measure_theory.simple_func.finset_sup_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [semilattice_sup β] [order_bot β] {f : γ → measure_theory.simple_func α β} (s : finset γ) (a : α) :
⇑(s.sup f) a = s.sup (λ (c : γ), ⇑(f c) a)
source
noncomputable def measure_theory.simple_func.restrict {α : Type u_1} {β : Type u_2} [measurable_space α] [has_zero β] (f : measure_theory.simple_func α β) (s : set α) :
measure_theory.simple_func α β

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
source
theorem measure_theory.simple_func.restrict_of_not_measurable {α : Type u_1} {β : Type u_2} [measurable_space α] [has_zero β] {f : measure_theory.simple_func α β} {s : set α} (hs : ¬measurable_set s) :
f.restrict s = 0
source
@[simp]
theorem measure_theory.simple_func.coe_restrict {α : Type u_1} {β : Type u_2} [measurable_space α] [has_zero β] (f : measure_theory.simple_func α β) {s : set α} (hs : measurable_set s) :
⇑(f.restrict s) = s.indicator ⇑f
source
@[simp]
theorem measure_theory.simple_func.restrict_univ {α : Type u_1} {β : Type u_2} [measurable_space α] [has_zero β] (f : measure_theory.simple_func α β) :
f.restrict set.univ = f
source
@[simp]
theorem measure_theory.simple_func.restrict_empty {α : Type u_1} {β : Type u_2} [measurable_space α] [has_zero β] (f : measure_theory.simple_func α β) :
f.restrict ∅ = 0
source
theorem measure_theory.simple_func.map_restrict_of_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [has_zero β] [has_zero γ] {g : β → γ} (hg : g 0 = 0) (f : measure_theory.simple_func α β) (s : set α) :
measure_theory.simple_func.map g (f.restrict s) = (measure_theory.simple_func.map g f).restrict s
source
theorem measure_theory.simple_func.map_coe_ennreal_restrict {α : Type u_1} [measurable_space α] (f : measure_theory.simple_func α nnreal) (s : set α) :
measure_theory.simple_func.map coe (f.restrict s) = (measure_theory.simple_func.map coe f).restrict s
source
theorem measure_theory.simple_func.map_coe_nnreal_restrict {α : Type u_1} [measurable_space α] (f : measure_theory.simple_func α nnreal) (s : set α) :
measure_theory.simple_func.map coe (f.restrict s) = (measure_theory.simple_func.map coe f).restrict s
source
theorem measure_theory.simple_func.restrict_apply {α : Type u_1} {β : Type u_2} [measurable_space α] [has_zero β] (f : measure_theory.simple_func α β) {s : set α} (hs : measurable_set s) (a : α) :
⇑(f.restrict s) a = s.indicator ⇑f a
source
theorem measure_theory.simple_func.restrict_preimage {α : Type u_1} {β : Type u_2} [measurable_space α] [has_zero β] (f : measure_theory.simple_func α β) {s : set α} (hs : measurable_set s) {t : set β} (ht : 0 ∉ t) :
⇑(f.restrict s) ⁻¹' t = s ∩ ⇑f ⁻¹' t
source
theorem measure_theory.simple_func.restrict_preimage_singleton {α : Type u_1} {β : Type u_2} [measurable_space α] [has_zero β] (f : measure_theory.simple_func α β) {s : set α} (hs : measurable_set s) {r : β} (hr : r ≠ 0) :
⇑(f.restrict s) ⁻¹' {r} = s ∩ ⇑f ⁻¹' {r}
source
theorem measure_theory.simple_func.mem_restrict_range {α : Type u_1} {β : Type u_2} [measurable_space α] [has_zero β] {r : β} {s : set α} {f : measure_theory.simple_func α β} (hs : measurable_set s) :
r ∈ (f.restrict s).range ↔ r = 0 ∧ s ≠ set.univ ∨ r ∈ ⇑f '' s
source
theorem measure_theory.simple_func.mem_image_of_mem_range_restrict {α : Type u_1} {β : Type u_2} [measurable_space α] [has_zero β] {r : β} {s : set α} {f : measure_theory.simple_func α β} (hr : r ∈ (f.restrict s).range) (h0 : r ≠ 0) :
r ∈ ⇑f '' s
source
theorem measure_theory.simple_func.restrict_mono {α : Type u_1} {β : Type u_2} [measurable_space α] [has_zero β] [preorder β] (s : set α) {f g : measure_theory.simple_func α β} (H : f ≤ g) :
f.restrict s ≤ g.restrict s
source
noncomputable def measure_theory.simple_func.approx {α : Type u_1} {β : Type u_2} [measurable_space α] [semilattice_sup β] [order_bot β] [has_zero β] (i : ℕ → β) (f : α → β) (n : ℕ) :
measure_theory.simple_func α β

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
source
theorem measure_theory.simple_func.approx_apply {α : Type u_1} {β : Type u_2} [measurable_space α] [semilattice_sup β] [order_bot β] [has_zero β] [topological_space β] [order_closed_topology β] [measurable_space β] [opens_measurable_space β] {i : ℕ → β} {f : α → β} {n : ℕ} (a : α) (hf : measurable f) :
⇑(measure_theory.simple_func.approx i f n) a = (finset.range n).sup (λ (k : ℕ), ite (i k ≤ f a) (i k) 0)
source
theorem measure_theory.simple_func.monotone_approx {α : Type u_1} {β : Type u_2} [measurable_space α] [semilattice_sup β] [order_bot β] [has_zero β] (i : ℕ → β) (f : α → β) :
monotone (measure_theory.simple_func.approx i f)
source
theorem measure_theory.simple_func.approx_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [semilattice_sup β] [order_bot β] [has_zero β] [topological_space β] [order_closed_topology β] [measurable_space β] [opens_measurable_space β] [measurable_space γ] {i : ℕ → β} {f : γ → β} {g : α → γ} {n : ℕ} (a : α) (hf : measurable f) (hg : measurable g) :
⇑(measure_theory.simple_func.approx i (f ∘ g) n) a = ⇑(measure_theory.simple_func.approx i f n) (g a)
source
theorem measure_theory.simple_func.supr_approx_apply {α : Type u_1} {β : Type u_2} [measurable_space α] [topological_space β] [complete_lattice β] [order_closed_topology β] [has_zero β] [measurable_space β] [opens_measurable_space β] (i : ℕ → β) (f : α → β) (a : α) (hf : measurable f) (h_zero : 0 = ⊥) :
(⨆ (n : ℕ), ⇑(measure_theory.simple_func.approx i f n) a) = ⨆ (k : ℕ) (h : i k ≤ f a), i k
source
noncomputable def measure_theory.simple_func.ennreal_rat_embed (n : ℕ) :
ennreal

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

Equations
source
theorem measure_theory.simple_func.ennreal_rat_embed_encode (q : ℚ) :
measure_theory.simple_func.ennreal_rat_embed (encodable.encode q) = ↑(↑q.to_nnreal)
source
noncomputable def measure_theory.simple_func.eapprox {α : Type u_1} [measurable_space α] :
(α → ennreal) → ℕ → measure_theory.simple_func α ennreal

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

Equations
source
theorem measure_theory.simple_func.eapprox_lt_top {α : Type u_1} [measurable_space α] (f : α → ennreal) (n : ℕ) (a : α) :
⇑(measure_theory.simple_func.eapprox f n) a < ⊤
source
theorem measure_theory.simple_func.monotone_eapprox {α : Type u_1} [measurable_space α] (f : α → ennreal) :
monotone (measure_theory.simple_func.eapprox f)
source
theorem measure_theory.simple_func.supr_eapprox_apply {α : Type u_1} [measurable_space α] (f : α → ennreal) (hf : measurable f) (a : α) :
(⨆ (n : ℕ), ⇑(measure_theory.simple_func.eapprox f n) a) = f a
source
theorem measure_theory.simple_func.eapprox_comp {α : Type u_1} {γ : Type u_3} [measurable_space α] [measurable_space γ] {f : γ → ennreal} {g : α → γ} {n : ℕ} (hf : measurable f) (hg : measurable g) :
⇑(measure_theory.simple_func.eapprox (f ∘ g) n) = ⇑(measure_theory.simple_func.eapprox f n) ∘ g
source
noncomputable def measure_theory.simple_func.eapprox_diff {α : Type u_1} [measurable_space α] (f : α → ennreal) (n : ℕ) :
measure_theory.simple_func α nnreal

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

Equations
source
theorem measure_theory.simple_func.sum_eapprox_diff {α : Type u_1} [measurable_space α] (f : α → ennreal) (n : ℕ) (a : α) :
(finset.range (n + 1)).sum (λ (k : ℕ), ↑(⇑(measure_theory.simple_func.eapprox_diff f k) a)) = ⇑(measure_theory.simple_func.eapprox f n) a
source
theorem measure_theory.simple_func.tsum_eapprox_diff {α : Type u_1} [measurable_space α] (f : α → ennreal) (hf : measurable f) (a : α) :
∑' (n : ℕ), ↑(⇑(measure_theory.simple_func.eapprox_diff f n) a) = f a
source
noncomputable def measure_theory.simple_func.lintegral {α : Type u_1} {m : measurable_space α} (f : measure_theory.simple_func α ennreal) (μ : measure_theory.measure α) :
ennreal

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

Equations
source
theorem measure_theory.simple_func.lintegral_eq_of_subset {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : measure_theory.simple_func α ennreal) {s : finset ennreal} (hs : ∀ (x : α), ⇑f x ≠ 0 → ⇑μ (⇑f ⁻¹' {⇑f x}) ≠ 0 → ⇑f x ∈ s) :
f.lintegral μ = s.sum (λ (x : ennreal), x * ⇑μ (⇑f ⁻¹' {x}))
source
theorem measure_theory.simple_func.lintegral_eq_of_subset' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : measure_theory.simple_func α ennreal) {s : finset ennreal} (hs : f.range \ {0} ⊆ s) :
f.lintegral μ = s.sum (λ (x : ennreal), x * ⇑μ (⇑f ⁻¹' {x}))
source
theorem measure_theory.simple_func.map_lintegral {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} (g : β → ennreal) (f : measure_theory.simple_func α β) :
(measure_theory.simple_func.map g f).lintegral μ = f.range.sum (λ (x : β), g x * ⇑μ (⇑f ⁻¹' {x}))

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

source
theorem measure_theory.simple_func.add_lintegral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f g : measure_theory.simple_func α ennreal) :
(f + g).lintegral μ = f.lintegral μ + g.lintegral μ
source
theorem measure_theory.simple_func.const_mul_lintegral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : measure_theory.simple_func α ennreal) (x : ennreal) :
(measure_theory.simple_func.const α x * f).lintegral μ = x * f.lintegral μ
source
noncomputable def measure_theory.simple_func.lintegralₗ {α : Type u_1} {m : measurable_space α} :
measure_theory.simple_func α ennreal →ₗ[ennreal] measure_theory.measure α →ₗ[ennreal] ennreal

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

Equations
source
@[simp]
theorem measure_theory.simple_func.zero_lintegral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} :
0.lintegral μ = 0
source
theorem measure_theory.simple_func.lintegral_add {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} (f : measure_theory.simple_func α ennreal) :
f.lintegral (μ + ν) = f.lintegral μ + f.lintegral ν
source
theorem measure_theory.simple_func.lintegral_smul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : measure_theory.simple_func α ennreal) (c : ennreal) :
f.lintegral (c • μ) = c • f.lintegral μ
source
@[simp]
theorem measure_theory.simple_func.lintegral_zero {α : Type u_1} [measurable_space α] (f : measure_theory.simple_func α ennreal) :
f.lintegral 0 = 0
source
theorem measure_theory.simple_func.lintegral_sum {α : Type u_1} {m : measurable_space α} {ι : Type u_2} (f : measure_theory.simple_func α ennreal) (μ : ι → measure_theory.measure α) :
f.lintegral (measure_theory.measure.sum μ) = ∑' (i : ι), f.lintegral (μ i)
source
theorem measure_theory.simple_func.restrict_lintegral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : measure_theory.simple_func α ennreal) {s : set α} (hs : measurable_set s) :
(f.restrict s).lintegral μ = f.range.sum (λ (r : ennreal), r * ⇑μ (⇑f ⁻¹' {r} ∩ s))
source
theorem measure_theory.simple_func.lintegral_restrict {α : Type u_1} {m : measurable_space α} (f : measure_theory.simple_func α ennreal) (s : set α) (μ : measure_theory.measure α) :
f.lintegral (μ.restrict s) = f.range.sum (λ (y : ennreal), y * ⇑μ (⇑f ⁻¹' {y} ∩ s))
source
theorem measure_theory.simple_func.restrict_lintegral_eq_lintegral_restrict {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : measure_theory.simple_func α ennreal) {s : set α} (hs : measurable_set s) :
(f.restrict s).lintegral μ = f.lintegral (μ.restrict s)
source
theorem measure_theory.simple_func.const_lintegral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (c : ennreal) :
(measure_theory.simple_func.const α c).lintegral μ = c * ⇑μ set.univ
source
theorem measure_theory.simple_func.const_lintegral_restrict {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (c : ennreal) (s : set α) :
(measure_theory.simple_func.const α c).lintegral (μ.restrict s) = c * ⇑μ s
source
theorem measure_theory.simple_func.restrict_const_lintegral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (c : ennreal) {s : set α} (hs : measurable_set s) :
((measure_theory.simple_func.const α c).restrict s).lintegral μ = c * ⇑μ s
source
theorem measure_theory.simple_func.le_sup_lintegral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f g : measure_theory.simple_func α ennreal) :
f.lintegral μ ⊔ g.lintegral μ ≤ (f ⊔ g).lintegral μ
source
theorem measure_theory.simple_func.lintegral_mono {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} {f g : measure_theory.simple_func α ennreal} (hfg : f ≤ g) (hμν : μ ≤ ν) :
f.lintegral μ ≤ g.lintegral ν

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

source
theorem measure_theory.simple_func.lintegral_eq_of_measure_preimage {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [measurable_space β] {f : measure_theory.simple_func α ennreal} {g : measure_theory.simple_func β ennreal} {ν : measure_theory.measure β} (H : ∀ (y : ennreal), ⇑μ (⇑f ⁻¹' {y}) = ⇑ν (⇑g ⁻¹' {y})) :
f.lintegral μ = g.lintegral ν

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

source
theorem measure_theory.simple_func.lintegral_congr {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f g : measure_theory.simple_func α ennreal} (h : ⇑f =ᵐ[μ] ⇑g) :
f.lintegral μ = g.lintegral μ

If two simple functions are equal a.e., then their lintegrals are equal.

source
theorem measure_theory.simple_func.lintegral_map' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} [measurable_space β] {μ' : measure_theory.measure β} (f : measure_theory.simple_func α ennreal) (g : measure_theory.simple_func β ennreal) (m' : α → β) (eq : ∀ (a : α), ⇑f a = ⇑g (m' a)) (h : ∀ (s : set β), measurable_set s → ⇑μ' s = ⇑μ (m' ⁻¹' s)) :
f.lintegral μ = g.lintegral μ'
source
theorem measure_theory.simple_func.lintegral_map {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} [measurable_space β] (g : measure_theory.simple_func β ennreal) {f : α → β} (hf : measurable f) :
g.lintegral (measure_theory.measure.map f μ) = (g.comp f hf).lintegral μ
source
theorem measure_theory.simple_func.support_eq {α : Type u_1} {β : Type u_2} [measurable_space α] [has_zero β] (f : measure_theory.simple_func α β) :
function.support ⇑f = ⋃ (y : β) (H : y ∈ finset.filter (λ (y : β), y ≠ 0) f.range), ⇑f ⁻¹' {y}
source
theorem measure_theory.simple_func.measurable_set_support {α : Type u_1} {β : Type u_2} [has_zero β] [measurable_space α] (f : measure_theory.simple_func α β) :
measurable_set (function.support ⇑f)
source
@[protected]
def measure_theory.simple_func.fin_meas_supp {α : Type u_1} {β : Type u_2} [has_zero β] {m : measurable_space α} (f : measure_theory.simple_func α β) (μ : 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
source
theorem measure_theory.simple_func.fin_meas_supp_iff_support {α : Type u_1} {β : Type u_2} {m : measurable_space α} [has_zero β] {μ : measure_theory.measure α} {f : measure_theory.simple_func α β} :
f.fin_meas_supp μ ↔ ⇑μ (function.support ⇑f) < ⊤
source
theorem measure_theory.simple_func.fin_meas_supp_iff {α : Type u_1} {β : Type u_2} {m : measurable_space α} [has_zero β] {μ : measure_theory.measure α} {f : measure_theory.simple_func α β} :
f.fin_meas_supp μ ↔ ∀ (y : β), y ≠ 0 → ⇑μ (⇑f ⁻¹' {y}) < ⊤
source
theorem measure_theory.simple_func.fin_meas_supp.meas_preimage_singleton_ne_zero {α : Type u_1} {β : Type u_2} {m : measurable_space α} [has_zero β] {μ : measure_theory.measure α} {f : measure_theory.simple_func α β} (h : f.fin_meas_supp μ) {y : β} (hy : y ≠ 0) :
⇑μ (⇑f ⁻¹' {y}) < ⊤
source
@[protected]
theorem measure_theory.simple_func.fin_meas_supp.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} [has_zero β] [has_zero γ] {μ : measure_theory.measure α} {f : measure_theory.simple_func α β} {g : β → γ} (hf : f.fin_meas_supp μ) (hg : g 0 = 0) :
(measure_theory.simple_func.map g f).fin_meas_supp μ
source
theorem measure_theory.simple_func.fin_meas_supp.of_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} [has_zero β] [has_zero γ] {μ : measure_theory.measure α} {f : measure_theory.simple_func α β} {g : β → γ} (h : (measure_theory.simple_func.map g f).fin_meas_supp μ) (hg : ∀ (b : β), g b = 0 → b = 0) :
f.fin_meas_supp μ
source
theorem measure_theory.simple_func.fin_meas_supp.map_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} [has_zero β] [has_zero γ] {μ : measure_theory.measure α} {f : measure_theory.simple_func α β} {g : β → γ} (hg : ∀ {b : β}, g b = 0 ↔ b = 0) :
(measure_theory.simple_func.map g f).fin_meas_supp μ ↔ f.fin_meas_supp μ
source
@[protected]
theorem measure_theory.simple_func.fin_meas_supp.pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} [has_zero β] [has_zero γ] {μ : measure_theory.measure α} {f : measure_theory.simple_func α β} {g : measure_theory.simple_func α γ} (hf : f.fin_meas_supp μ) (hg : g.fin_meas_supp μ) :
(f.pair g).fin_meas_supp μ
source
@[protected]
theorem measure_theory.simple_func.fin_meas_supp.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m : measurable_space α} [has_zero β] [has_zero γ] {μ : measure_theory.measure α} {f : measure_theory.simple_func α β} [has_zero δ] (hf : f.fin_meas_supp μ) {g : measure_theory.simple_func α γ} (hg : g.fin_meas_supp μ) {op : β → γ → δ} (H : op 0 0 = 0) :
(measure_theory.simple_func.map (function.uncurry op) (f.pair g)).fin_meas_supp μ
source
@[protected]
theorem measure_theory.simple_func.fin_meas_supp.add {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} [add_monoid β] {f g : measure_theory.simple_func α β} (hf : f.fin_meas_supp μ) (hg : g.fin_meas_supp μ) :
(f + g).fin_meas_supp μ
source
@[protected]
theorem measure_theory.simple_func.fin_meas_supp.mul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} [monoid_with_zero β] {f g : measure_theory.simple_func α β} (hf : f.fin_meas_supp μ) (hg : g.fin_meas_supp μ) :
(f * g).fin_meas_supp μ
source
theorem measure_theory.simple_func.fin_meas_supp.lintegral_lt_top {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : measure_theory.simple_func α ennreal} (hm : f.fin_meas_supp μ) (hf : ∀ᵐ (a : α) ∂μ, ⇑f a ≠ ⊤) :
f.lintegral μ < ⊤
source
theorem measure_theory.simple_func.fin_meas_supp.of_lintegral_ne_top {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : measure_theory.simple_func α ennreal} (h : f.lintegral μ ≠ ⊤) :
f.fin_meas_supp μ
source
theorem measure_theory.simple_func.fin_meas_supp.iff_lintegral_lt_top {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : measure_theory.simple_func α ennreal} (hf : ∀ᵐ (a : α) ∂μ, ⇑f a ≠ ⊤) :
f.fin_meas_supp μ ↔ f.lintegral μ < ⊤
source
@[protected]
theorem measure_theory.simple_func.induction {α : Type u_1} {γ : Type u_2} [measurable_space α] [add_monoid γ] {P : measure_theory.simple_func α γ → Prop} (h_ind : ∀ (c : γ) {s : set α} (hs : measurable_set s), P (measure_theory.simple_func.piecewise s hs (measure_theory.simple_func.const α c) (measure_theory.simple_func.const α 0))) (h_add : ∀ ⦃f g : measure_theory.simple_func α γ⦄, disjoint (function.support ⇑f) (function.support ⇑g) → P f → P g → P (f + g)) (f : measure_theory.simple_func α γ) :
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)

source
@[irreducible]
noncomputable def measure_theory.lintegral {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) (f : α → ennreal) :
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.

source
theorem measure_theory.simple_func.lintegral_eq_lintegral {α : Type u_1} {m : measurable_space α} (f : measure_theory.simple_func α ennreal) (μ : measure_theory.measure α) :
∫⁻ (a : α), ⇑f a ∂μ = f.lintegral μ
source
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 ∂ν
source
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 ∂μ
source
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) ∂μ
source
theorem measure_theory.supr_lintegral_measurable_le_eq_lintegral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : α → ennreal) :
(⨆ (g : α → ennreal) (g_meas : measurable g) (hg : g ≤ f), ∫⁻ (a : α), g a ∂μ) = ∫⁻ (a : α), f a ∂μ
source
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 ∂μ
source
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 ∂μ
source
theorem measure_theory.monotone_lintegral {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) :
monotone (measure_theory.lintegral μ)
source
@[simp]
theorem measure_theory.lintegral_const {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (c : ennreal) :
∫⁻ (a : α), c ∂μ = c * ⇑μ set.univ
source
theorem measure_theory.lintegral_zero {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} :
∫⁻ (a : α), 0 ∂μ = 0
source
theorem measure_theory.lintegral_zero_fun {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} :
measure_theory.lintegral μ 0 = 0
source
@[simp]
theorem measure_theory.lintegral_one {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} :
∫⁻ (a : α), 1 ∂μ = ⇑μ set.univ
source
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
source
theorem measure_theory.set_lintegral_one {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (s : set α) :
∫⁻ (a : α) in s, 1 ∂μ = ⇑μ s
source
theorem measure_theory.set_lintegral_const_lt_top {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] (s : set α) {c : ennreal} (hc : c ≠ ⊤) :
∫⁻ (a : α) in s, c ∂μ < ⊤
source
theorem measure_theory.lintegral_const_lt_top {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {c : ennreal} (hc : c ≠ ⊤) :
∫⁻ (a : α), c ∂μ < ⊤
source
theorem measure_theory.exists_measurable_le_lintegral_eq {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) (f : α → ennreal) :
∃ (g : α → ennreal), measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ

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

source
theorem measure_theory.lintegral_eq_nnreal {α : Type u_1} {m : measurable_space α} (f : α → ennreal) (μ : measure_theory.measure α) :
∫⁻ (a : α), f a ∂μ = ⨆ (φ : measure_theory.simple_func α nnreal) (hf : ∀ (x : α), ↑(⇑φ x) ≤ f x), (measure_theory.simple_func.map coe φ).lintegral μ

∫⁻ 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.

source
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) :
∃ (φ : measure_theory.simple_func α nnreal), (∀ (x : α), ↑(⇑φ x) ≤ f x) ∧ ∀ (ψ : measure_theory.simple_func α nnreal), (∀ (x : α), ↑(⇑ψ x) ≤ f x) → (measure_theory.simple_func.map coe (ψ - φ)).lintegral μ < ε
source
theorem measure_theory.supr_lintegral_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {ι : Sort u_2} (f : ι → α → ennreal) :
(⨆ (i : ι), ∫⁻ (a : α), f i a ∂μ) ≤ ∫⁻ (a : α), (⨆ (i : ι), f i a) ∂μ
source
theorem measure_theory.supr₂_lintegral_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {ι : Sort u_2} {ι' : ι → Sort u_3} (f : Π (i : ι), ι' i → α → ennreal) :
(⨆ (i : ι) (j : ι' i), ∫⁻ (a : α), f i j a ∂μ) ≤ ∫⁻ (a : α), (⨆ (i : ι) (j : ι' i), f i j a) ∂μ
source
theorem measure_theory.le_infi_lintegral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {ι : Sort u_2} (f : ι → α → ennreal) :
∫⁻ (a : α), (⨅ (i : ι), f i a) ∂μ ≤ ⨅ (i : ι), ∫⁻ (a : α), f i a ∂μ
source
theorem measure_theory.le_infi₂_lintegral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {ι : Sort u_2} {ι' : ι → Sort u_3} (f : Π (i : ι), ι' i → α → ennreal) :
∫⁻ (a : α), (⨅ (i : ι) (h : ι' i), f i h a) ∂μ ≤ ⨅ (i : ι) (h : ι' i), ∫⁻ (a : α), f i h a ∂μ
source
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 ∂μ
source
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 ∂μ
source
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 ∂μ
source
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 ∂μ
source
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 ∂μ
source
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 ∂μ
source
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 ∂μ
source
theorem measure_theory.lintegral_to_real_le_lintegral_nnnorm {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : α → ℝ) :
∫⁻ (x : α), ennreal.of_real (f x) ∂μ ≤ ∫⁻ (x : α), ↑∥f x∥₊ ∂μ
source
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) ∂μ
source
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) ∂μ
source
theorem measure_theory.lintegral_supr {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : ℕ → α → ennreal} (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.

source
theorem measure_theory.lintegral_supr' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : ℕ → α → ennreal} (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.

source
theorem measure_theory.lintegral_tendsto_of_tendsto_of_monotone {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : ℕ → α → ennreal} {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

source
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 : ℕ), (measure_theory.simple_func.eapprox f n).lintegral μ
source
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 δ.

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

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

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

source
theorem measure_theory.lintegral_add_left' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → ennreal} (hf : ae_measurable f μ) (g : α → ennreal) :
∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
source
theorem measure_theory.lintegral_add_right' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : α → ennreal) {g : α → ennreal} (hg : ae_measurable g μ) :
∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
source
@[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.

source
@[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 ∂μ
source
@[simp]
theorem measure_theory.lintegral_sum_measure {α : Type u_1} {m : measurable_space α} {ι : Type u_2} (f : α → ennreal) (μ : ι → measure_theory.measure α) :
∫⁻ (a : α), f a ∂measure_theory.measure.sum μ = ∑' (i : ι), ∫⁻ (a : α), f a ∂μ i
source
theorem measure_theory.has_sum_lintegral_measure {α : Type u_1} {ι : Type u_2} {m : measurable_space α} (f : α → ennreal) (μ : ι → measure_theory.measure α) :
has_sum (λ (i : ι), ∫⁻ (a : α), f a ∂μ i) (∫⁻ (a : α), f a ∂measure_theory.measure.sum μ)
source
@[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 ∂ν
source
@[simp]
theorem measure_theory.lintegral_finset_sum_measure {α : Type u_1} {ι : Type u_2} {m : measurable_space α} (s : finset ι) (f : α → ennreal) (μ : ι → measure_theory.measure α) :
∫⁻ (a : α), f a ∂s.sum (λ (i : ι), μ i) = s.sum (λ (i : ι), ∫⁻ (a : α), f a ∂μ i)
source
@[simp]
theorem measure_theory.lintegral_zero_measure {α : Type u_1} {m : measurable_space α} (f : α → ennreal) :
∫⁻ (a : α), f a ∂0 = 0
source
theorem measure_theory.set_lintegral_empty {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : α → ennreal) :
∫⁻ (x : α) in ∅, f x ∂μ = 0
source
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 ∂μ
source
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
source
theorem measure_theory.lintegral_finset_sum' {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} (s : finset β) {f : β → α → ennreal} (hf : ∀ (b : β), b ∈ s → ae_measurable (f b) μ) :
∫⁻ (a : α), s.sum (λ (b : β), f b a) ∂μ = s.sum (λ (b : β), ∫⁻ (a : α), f b a ∂μ)
source
theorem measure_theory.lintegral_finset_sum {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} (s : finset β) {f : β → α → ennreal} (hf : ∀ (b : β), b ∈ s → measurable (f b)) :
∫⁻ (a : α), s.sum (λ (b : β), f b a) ∂μ = s.sum (λ (b : β), ∫⁻ (a : α), f b a ∂μ)
source
@[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 ∂μ
source
theorem measure_theory.lintegral_const_mul'' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (r : ennreal) {f : α → ennreal} (hf : ae_measurable f μ) :
∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
source
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 ∂μ
source
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 ∂μ
source
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
source
theorem measure_theory.lintegral_mul_const'' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (r : ennreal) {f : α → ennreal} (hf : ae_measurable f μ) :
∫⁻ (a : α), f a * r ∂μ = ∫⁻ (a : α), f a ∂μ * r
source
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 ∂μ
source
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
source
theorem measure_theory.lintegral_lintegral_mul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} [measurable_space β] {ν : measure_theory.measure β} {f : α → ennreal} {g : β → ennreal} (hf : ae_measurable f μ) (hg : ae_measurable g ν) :
∫⁻ (x : α), ∫⁻ (y : β), f x * g y ∂ν ∂μ = ∫⁻ (x : α), f x ∂μ * ∫⁻ (y : β), g y ∂ν
source
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) ∂μ
source
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 : β → γ → ennreal) :
∫⁻ (a : α), g (f₁ a) (f₂ a) ∂μ = ∫⁻ (a : α), g (f₁' a) (f₂' a) ∂μ
source
@[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 ∂μ
source
theorem measure_theory.lintegral_indicator₀ {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : α → ennreal) {s : set α} (hs : measure_theory.null_measurable_set s μ) :
∫⁻ (a : α), s.indicator f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
source
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}
source
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 : ae_measurable g μ) (ε : 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.

source
theorem measure_theory.mul_meas_ge_le_lintegral₀ {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → ennreal} (hf : ae_measurable f μ) (ε : ennreal) :
ε * ⇑μ {x : α | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ

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

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

source
theorem measure_theory.lintegral_eq_top_of_measure_eq_top_pos {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → ennreal} (hf : ae_measurable f μ) (hμf : 0 < ⇑μ {x : α | f x = ⊤}) :
∫⁻ (x : α), f x ∂μ = ⊤
source
theorem measure_theory.meas_ge_le_lintegral_div {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → ennreal} (hf : ae_measurable f μ) {ε : ennreal} (hε : ε ≠ 0) (hε' : ε ≠ ⊤) :
⇑μ {x : α | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ / ε

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

source
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 : ae_measurable g μ) (hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ) :
f =ᵐ[μ] g
source
@[simp]
theorem measure_theory.lintegral_eq_zero_iff' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → ennreal} (hf : ae_measurable f μ) :
∫⁻ (a : α), f a ∂μ = 0 ↔ f =ᵐ[μ] 0
source
@[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
source
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 < ⇑μ (function.support f)
source
theorem measure_theory.lintegral_supr_ae {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : ℕ → α → ennreal} (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

source
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 ∂μ
source
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 ∂μ
source
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 : ae_measurable g μ) (hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤) (h_le : f ≤ᵐ[μ] g) (h : ∃ᵐ (x : α) ∂μ, f x ≠ g x) :
∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ
source
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 : ae_measurable g μ) (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 ∂μ
source
theorem measure_theory.lintegral_strict_mono {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α → ennreal} (hμ : μ ≠ 0) (hg : ae_measurable g μ) (hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤) (h : ∀ᵐ (x : α) ∂μ, f x < g x) :
∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ
source
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 ∂μ
source
theorem measure_theory.lintegral_infi_ae {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : ℕ → α → ennreal} (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

source
theorem measure_theory.lintegral_infi {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : ℕ → α → ennreal} (h_meas : ∀ (n : ℕ), measurable (f n)) (h_anti : antitone f) (h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤) :
∫⁻ (a : α), (⨅ (n : ℕ), f n a) ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Monotone convergence theorem for nonincreasing sequences of functions

source
theorem measure_theory.lintegral_liminf_le' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : ℕ → α → ennreal} (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

source
theorem measure_theory.lintegral_liminf_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : ℕ → α → ennreal} (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

source
theorem measure_theory.limsup_lintegral_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : ℕ → α → ennreal} {g : α → ennreal} (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)