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 functionf : α → ℝ≥0∞with respect to a measureμ;∫⁻ x, f x: integral of a functionf : α → ℝ≥0∞with respect to the canonical measurevolumeonα;∫⁻ x in s, f x ∂μ: integral of a functionf : α → ℝ≥0∞over a setswith respect to a measureμ, defined as∫⁻ x, f x ∂(μ.restrict s);∫⁻ x in s, f x: integral of a functionf : α → ℝ≥0∞over a setswith respect to the canonical measurevolume, defined as∫⁻ x, f x ∂(volume.restrict s).
structure
measure_theory.simple_func
(α : Type u)
[measurable_space α]
(β : Type v) :
Type (max u v)
- to_fun : α → β
- measurable_set_fiber' : ∀ (x : β), measurable_set (self.to_fun ⁻¹' {x})
- finite_range' : (set.range self.to_fun).finite
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.
@[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 α β), α → β)
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
@[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
theorem
measure_theory.simple_func.finite_range
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
(f : measure_theory.simple_func α β) :
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})
@[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 β.
@[simp]
theorem
measure_theory.simple_func.mem_range
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{f : measure_theory.simple_func α β}
{b : β} :
theorem
measure_theory.simple_func.mem_range_self
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
(f : measure_theory.simple_func α β)
(x : α) :
@[simp]
theorem
measure_theory.simple_func.coe_range
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
(f : measure_theory.simple_func α β) :
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) :
theorem
measure_theory.simple_func.forall_range_iff
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{f : measure_theory.simple_func α β}
{p : β → Prop} :
theorem
measure_theory.simple_func.exists_range_iff
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{f : measure_theory.simple_func α β}
{p : β → Prop} :
theorem
measure_theory.simple_func.preimage_eq_empty_iff
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
(f : measure_theory.simple_func α β)
(b : β) :
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 α β) :
Constant function as a simple_func.
Equations
- measure_theory.simple_func.const α b = {to_fun := λ (a : α), b, measurable_set_fiber' := _, finite_range' := _}
@[protected, instance]
def
measure_theory.simple_func.inhabited
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[inhabited β] :
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
@[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
@[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}
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}
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)}
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)
@[protected]
theorem
measure_theory.simple_func.measurable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(f : measure_theory.simple_func α β) :
A simple function is measurable
@[protected]
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 μ
@[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 β) :
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 α) :
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 α β) :
If-then-else as a simple_func.
Equations
- measure_theory.simple_func.piecewise s hs f g = {to_fun := s.piecewise ⇑f ⇑g (λ (j : α), classical.prop_decidable (j ∈ s)), measurable_set_fiber' := _, finite_range' := _}
@[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 α β) :
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 : α) :
@[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
@[simp]
theorem
measure_theory.simple_func.piecewise_univ
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
(f g : measure_theory.simple_func α β) :
@[simp]
theorem
measure_theory.simple_func.piecewise_empty
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
(f g : measure_theory.simple_func α β) :
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 α β) :
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}
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)
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 α γ) :
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
- f.bind g = {to_fun := λ (a : α), ⇑(g (⇑f a)) a, measurable_set_fiber' := _, finite_range' := _}
@[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 : α) :
def
measure_theory.simple_func.map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
(g : β → γ)
(f : measure_theory.simple_func α β) :
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}
[measurable_space α]
(g : β → γ)
(f : measure_theory.simple_func α β)
(a : α) :
⇑(measure_theory.simple_func.map 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}
[measurable_space α]
(g : β → γ)
(h : γ → δ)
(f : measure_theory.simple_func α β) :
@[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
@[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
@[simp]
theorem
measure_theory.simple_func.map_const
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
(g : β → γ)
(b : β) :
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)
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)
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) :
Composition of a simple_fun and a measurable function is a simple_func.
Equations
- f.comp g hgm = {to_fun := ⇑f ∘ g, measurable_set_fiber' := _, finite_range' := _}
@[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) :
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) :
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 β γ) :
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
- f₁.extend g hg f₂ = {to_fun := function.extend g ⇑f₁ ⇑f₂, measurable_set_fiber' := _, finite_range' := _}
@[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 : α) :
@[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 β γ) :
@[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 β γ) :
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 α β) :
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
- f.seq g = f.bind (λ (f : β → γ), measure_theory.simple_func.map f g)
@[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 : α) :
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
- f.pair g = (measure_theory.simple_func.map prod.mk f).seq g
@[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 : α) :
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 γ) :
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 : γ) :
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
@[protected, instance]
def
measure_theory.simple_func.has_zero
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_zero β] :
Equations
@[protected, instance]
def
measure_theory.simple_func.has_add
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_add β] :
Equations
- measure_theory.simple_func.has_add = {add := λ (f g : measure_theory.simple_func α β), (measure_theory.simple_func.map has_add.add f).seq g}
@[protected, instance]
def
measure_theory.simple_func.has_mul
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_mul β] :
Equations
- measure_theory.simple_func.has_mul = {mul := λ (f g : measure_theory.simple_func α β), (measure_theory.simple_func.map has_mul.mul f).seq g}
@[protected, instance]
def
measure_theory.simple_func.has_sup
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_sup β] :
Equations
- measure_theory.simple_func.has_sup = {sup := λ (f g : measure_theory.simple_func α β), (measure_theory.simple_func.map has_sup.sup f).seq g}
@[protected, instance]
def
measure_theory.simple_func.has_inf
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_inf β] :
Equations
- measure_theory.simple_func.has_inf = {inf := λ (f g : measure_theory.simple_func α β), (measure_theory.simple_func.map has_inf.inf f).seq g}
@[protected, instance]
def
measure_theory.simple_func.has_le
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_le β] :
Equations
- measure_theory.simple_func.has_le = {le := λ (f g : measure_theory.simple_func α β), ∀ (a : α), ⇑f a ≤ ⇑g a}
@[simp, norm_cast]
theorem
measure_theory.simple_func.coe_zero
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_zero β] :
@[simp]
theorem
measure_theory.simple_func.const_zero
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_zero β] :
@[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 α β) :
@[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 α β) :
@[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 α β} :
@[simp]
theorem
measure_theory.simple_func.range_zero
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[nonempty α]
[has_zero β] :
@[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 α β) :
theorem
measure_theory.simple_func.eq_zero_of_mem_range_zero
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_zero β]
{y : β} :
theorem
measure_theory.simple_func.sup_apply
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_sup β]
(f g : measure_theory.simple_func α β)
(a : α) :
theorem
measure_theory.simple_func.mul_apply
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_mul β]
(f g : measure_theory.simple_func α β)
(a : α) :
theorem
measure_theory.simple_func.add_apply
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_add β]
(f g : measure_theory.simple_func α β)
(a : α) :
theorem
measure_theory.simple_func.add_eq_map₂
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_add β]
(f g : measure_theory.simple_func α β) :
theorem
measure_theory.simple_func.mul_eq_map₂
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_mul β]
(f g : measure_theory.simple_func α β) :
theorem
measure_theory.simple_func.sup_eq_map₂
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_sup β]
(f g : measure_theory.simple_func α β) :
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
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₂
@[protected, instance]
def
measure_theory.simple_func.add_monoid
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[add_monoid β] :
Equations
- measure_theory.simple_func.add_monoid = function.injective.add_monoid (λ (f : measure_theory.simple_func α β), show α → β, from ⇑f) measure_theory.simple_func.coe_injective measure_theory.simple_func.add_monoid._proof_1 measure_theory.simple_func.add_monoid._proof_2
@[protected, instance]
def
measure_theory.simple_func.add_comm_monoid
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[add_comm_monoid β] :
Equations
- measure_theory.simple_func.add_comm_monoid = function.injective.add_comm_monoid (λ (f : measure_theory.simple_func α β), show α → β, from ⇑f) measure_theory.simple_func.coe_injective measure_theory.simple_func.add_comm_monoid._proof_1 measure_theory.simple_func.add_comm_monoid._proof_2
@[protected, instance]
def
measure_theory.simple_func.has_neg
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_neg β] :
Equations
@[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 α β) :
@[protected, instance]
def
measure_theory.simple_func.has_sub
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_sub β] :
Equations
- measure_theory.simple_func.has_sub = {sub := λ (f g : measure_theory.simple_func α β), (measure_theory.simple_func.map has_sub.sub f).seq g}
@[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 α β) :
theorem
measure_theory.simple_func.sub_apply
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_sub β]
(f g : measure_theory.simple_func α β)
(x : α) :
@[protected, instance]
def
measure_theory.simple_func.add_group
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[add_group β] :
Equations
- measure_theory.simple_func.add_group = function.injective.add_group (λ (f : measure_theory.simple_func α β), show α → β, from ⇑f) measure_theory.simple_func.coe_injective measure_theory.simple_func.add_group._proof_1 measure_theory.simple_func.add_group._proof_2 measure_theory.simple_func.add_group._proof_3 measure_theory.simple_func.add_group._proof_4
@[protected, instance]
def
measure_theory.simple_func.add_comm_group
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[add_comm_group β] :
Equations
- measure_theory.simple_func.add_comm_group = function.injective.add_comm_group (λ (f : measure_theory.simple_func α β), show α → β, from ⇑f) measure_theory.simple_func.coe_injective measure_theory.simple_func.add_comm_group._proof_1 measure_theory.simple_func.add_comm_group._proof_2 measure_theory.simple_func.add_comm_group._proof_3 measure_theory.simple_func.add_comm_group._proof_4
@[protected, instance]
def
measure_theory.simple_func.has_scalar
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{K : Type u_5}
[has_scalar K β] :
has_scalar K (measure_theory.simple_func α β)
Equations
- measure_theory.simple_func.has_scalar = {smul := λ (k : K) (f : measure_theory.simple_func α β), measure_theory.simple_func.map (has_scalar.smul k) f}
@[simp]
theorem
measure_theory.simple_func.coe_smul
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{K : Type u_5}
[has_scalar K β]
(c : K)
(f : measure_theory.simple_func α β) :
theorem
measure_theory.simple_func.smul_apply
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{K : Type u_5}
[has_scalar K β]
(k : K)
(f : measure_theory.simple_func α β)
(a : α) :
@[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
- measure_theory.simple_func.module = function.injective.module K {to_fun := λ (f : measure_theory.simple_func α β), show α → β, from ⇑f, map_zero' := _, map_add' := _} measure_theory.simple_func.coe_injective measure_theory.simple_func.module._proof_3
theorem
measure_theory.simple_func.smul_eq_map
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{K : Type u_5}
[has_scalar K β]
(k : K)
(f : measure_theory.simple_func α β) :
k • f = measure_theory.simple_func.map (has_scalar.smul k) f
@[protected, instance]
def
measure_theory.simple_func.preorder
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[preorder β] :
Equations
- measure_theory.simple_func.preorder = {le := has_le.le measure_theory.simple_func.has_le, lt := λ (a b : measure_theory.simple_func α β), a ≤ b ∧ ¬b ≤ a, le_refl := _, le_trans := _, lt_iff_le_not_le := _}
@[protected, instance]
def
measure_theory.simple_func.partial_order
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[partial_order β] :
Equations
@[protected, instance]
def
measure_theory.simple_func.order_bot
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_le β]
[order_bot β] :
Equations
@[protected, instance]
def
measure_theory.simple_func.order_top
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_le β]
[order_top β] :
Equations
@[protected, instance]
def
measure_theory.simple_func.semilattice_inf
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[semilattice_inf β] :
Equations
- measure_theory.simple_func.semilattice_inf = {inf := has_inf.inf measure_theory.simple_func.has_inf, le := partial_order.le measure_theory.simple_func.partial_order, lt := partial_order.lt measure_theory.simple_func.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}
@[protected, instance]
def
measure_theory.simple_func.semilattice_sup
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[semilattice_sup β] :
Equations
- measure_theory.simple_func.semilattice_sup = {sup := has_sup.sup measure_theory.simple_func.has_sup, le := partial_order.le measure_theory.simple_func.partial_order, lt := partial_order.lt measure_theory.simple_func.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}
@[protected, instance]
def
measure_theory.simple_func.lattice
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[lattice β] :
Equations
- measure_theory.simple_func.lattice = {sup := semilattice_sup.sup measure_theory.simple_func.semilattice_sup, le := semilattice_sup.le measure_theory.simple_func.semilattice_sup, lt := semilattice_sup.lt measure_theory.simple_func.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf measure_theory.simple_func.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
@[protected, instance]
def
measure_theory.simple_func.bounded_order
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_le β]
[bounded_order β] :
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 : α) :
noncomputable
def
measure_theory.simple_func.restrict
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_zero β]
(f : measure_theory.simple_func α β)
(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 = dite (measurable_set s) (λ (hs : measurable_set s), measure_theory.simple_func.piecewise s hs f 0) (λ (hs : ¬measurable_set s), 0)
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) :
@[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) :
@[simp]
theorem
measure_theory.simple_func.restrict_univ
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_zero β]
(f : measure_theory.simple_func α β) :
@[simp]
theorem
measure_theory.simple_func.restrict_empty
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_zero β]
(f : measure_theory.simple_func α β) :
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
theorem
measure_theory.simple_func.map_coe_ennreal_restrict
{α : Type u_1}
[measurable_space α]
(f : measure_theory.simple_func α ℝ≥0)
(s : set α) :
theorem
measure_theory.simple_func.map_coe_nnreal_restrict
{α : Type u_1}
[measurable_space α]
(f : measure_theory.simple_func α ℝ≥0)
(s : set α) :
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 : α) :
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) :
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) :
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) :
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) :
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) :
noncomputable
def
measure_theory.simple_func.approx
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[semilattice_sup β]
[order_bot β]
[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
- measure_theory.simple_func.approx i f n = (finset.range n).sup (λ (k : ℕ), (measure_theory.simple_func.const α (i k)).restrict {a : α | i k ≤ f a})
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)
theorem
measure_theory.simple_func.monotone_approx
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[semilattice_sup β]
[order_bot β]
[has_zero β]
(i : ℕ → β)
(f : α → β) :
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)
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 = ⊥) :
A sequence of ℝ≥0∞s such that its range is the set of non-negative rational numbers.
Equations
noncomputable
def
measure_theory.simple_func.eapprox
{α : Type u_1}
[measurable_space α] :
(α → ℝ≥0∞) → ℕ → measure_theory.simple_func α ℝ≥0∞
Approximate a function α → ℝ≥0∞ by a sequence of simple functions.
theorem
measure_theory.simple_func.eapprox_lt_top
{α : Type u_1}
[measurable_space α]
(f : α → ℝ≥0∞)
(n : ℕ)
(a : α) :
⇑(measure_theory.simple_func.eapprox f n) a < ⊤
theorem
measure_theory.simple_func.monotone_eapprox
{α : Type u_1}
[measurable_space α]
(f : α → ℝ≥0∞) :
theorem
measure_theory.simple_func.supr_eapprox_apply
{α : Type u_1}
[measurable_space α]
(f : α → ℝ≥0∞)
(hf : measurable f)
(a : α) :
(⨆ (n : ℕ), ⇑(measure_theory.simple_func.eapprox f n) a) = f a
theorem
measure_theory.simple_func.eapprox_comp
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{f : γ → ℝ≥0∞}
{g : α → γ}
{n : ℕ}
(hf : measurable f)
(hg : measurable g) :
⇑(measure_theory.simple_func.eapprox (f ∘ g) n) = ⇑(measure_theory.simple_func.eapprox f n) ∘ g
noncomputable
def
measure_theory.simple_func.eapprox_diff
{α : Type u_1}
[measurable_space α]
(f : α → ℝ≥0∞)
(n : ℕ) :
Approximate a function α → ℝ≥0∞ by a series of simple functions taking their values
in ℝ≥0.
Equations
- measure_theory.simple_func.eapprox_diff f (n + 1) = measure_theory.simple_func.map ennreal.to_nnreal (measure_theory.simple_func.eapprox f (n + 1) - measure_theory.simple_func.eapprox f n)
- measure_theory.simple_func.eapprox_diff f 0 = measure_theory.simple_func.map ennreal.to_nnreal (measure_theory.simple_func.eapprox f 0)
theorem
measure_theory.simple_func.sum_eapprox_diff
{α : Type u_1}
[measurable_space α]
(f : α → ℝ≥0∞)
(n : ℕ)
(a : α) :
∑ (k : ℕ) in finset.range (n + 1), ↑(⇑(measure_theory.simple_func.eapprox_diff f k) a) = ⇑(measure_theory.simple_func.eapprox f n) a
theorem
measure_theory.simple_func.tsum_eapprox_diff
{α : Type u_1}
[measurable_space α]
(f : α → ℝ≥0∞)
(hf : measurable f)
(a : α) :
∑' (n : ℕ), ↑(⇑(measure_theory.simple_func.eapprox_diff f n) a) = f a
noncomputable
def
measure_theory.simple_func.lintegral
{α : Type u_1}
{m : measurable_space α}
(f : measure_theory.simple_func α ℝ≥0∞)
(μ : measure_theory.measure α) :
Integral of a simple function whose codomain is ℝ≥0∞.
theorem
measure_theory.simple_func.lintegral_eq_of_subset
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(f : measure_theory.simple_func α ℝ≥0∞)
{s : finset ℝ≥0∞}
(hs : ∀ (x : α), ⇑f x ≠ 0 → ⇑μ (⇑f ⁻¹' {⇑f x}) ≠ 0 → ⇑f x ∈ s) :
theorem
measure_theory.simple_func.lintegral_eq_of_subset'
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(f : measure_theory.simple_func α ℝ≥0∞)
{s : finset ℝ≥0∞}
(hs : f.range \ {0} ⊆ s) :
theorem
measure_theory.simple_func.map_lintegral
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
(g : β → ℝ≥0∞)
(f : measure_theory.simple_func α β) :
Calculate the integral of (g ∘ f), where g : β → ℝ≥0∞ and f : α →ₛ β.
theorem
measure_theory.simple_func.add_lintegral
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(f g : measure_theory.simple_func α ℝ≥0∞) :
theorem
measure_theory.simple_func.const_mul_lintegral
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(f : measure_theory.simple_func α ℝ≥0∞)
(x : ℝ≥0∞) :
Integral of a simple function α →ₛ ℝ≥0∞ as a bilinear map.
@[simp]
theorem
measure_theory.simple_func.zero_lintegral
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α} :
theorem
measure_theory.simple_func.lintegral_add
{α : Type u_1}
{m : measurable_space α}
{μ ν : measure_theory.measure α}
(f : measure_theory.simple_func α ℝ≥0∞) :
theorem
measure_theory.simple_func.lintegral_smul
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(f : measure_theory.simple_func α ℝ≥0∞)
(c : ℝ≥0∞) :
@[simp]
theorem
measure_theory.simple_func.lintegral_zero
{α : Type u_1}
[measurable_space α]
(f : measure_theory.simple_func α ℝ≥0∞) :
theorem
measure_theory.simple_func.lintegral_sum
{α : Type u_1}
{m : measurable_space α}
{ι : Type u_2}
(f : measure_theory.simple_func α ℝ≥0∞)
(μ : ι → measure_theory.measure α) :
f.lintegral (measure_theory.measure.sum μ) = ∑' (i : ι), f.lintegral (μ i)
theorem
measure_theory.simple_func.restrict_lintegral
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(f : measure_theory.simple_func α ℝ≥0∞)
{s : set α}
(hs : measurable_set s) :
theorem
measure_theory.simple_func.lintegral_restrict
{α : Type u_1}
{m : measurable_space α}
(f : measure_theory.simple_func α ℝ≥0∞)
(s : set α)
(μ : measure_theory.measure α) :
theorem
measure_theory.simple_func.restrict_lintegral_eq_lintegral_restrict
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(f : measure_theory.simple_func α ℝ≥0∞)
{s : set α}
(hs : measurable_set s) :
theorem
measure_theory.simple_func.const_lintegral
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(c : ℝ≥0∞) :
theorem
measure_theory.simple_func.const_lintegral_restrict
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(c : ℝ≥0∞)
(s : set α) :
theorem
measure_theory.simple_func.restrict_const_lintegral
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(c : ℝ≥0∞)
{s : set α}
(hs : measurable_set s) :
theorem
measure_theory.simple_func.le_sup_lintegral
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(f g : measure_theory.simple_func α ℝ≥0∞) :
theorem
measure_theory.simple_func.lintegral_mono
{α : Type u_1}
{m : measurable_space α}
{μ ν : measure_theory.measure α}
{f g : measure_theory.simple_func α ℝ≥0∞}
(hfg : f ≤ g)
(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}
{m : measurable_space α}
{μ : measure_theory.measure α}
[measurable_space β]
{f : measure_theory.simple_func α ℝ≥0∞}
{g : measure_theory.simple_func β ℝ≥0∞}
{ν : 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}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f g : measure_theory.simple_func α ℝ≥0∞}
(h : ⇑f =ᵐ[μ] ⇑g) :
If two simple functions are equal a.e., then their lintegrals are equal.
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 α ℝ≥0∞)
(g : measure_theory.simple_func β ℝ≥0∞)
(m' : α → β)
(eq : ∀ (a : α), ⇑f a = ⇑g (m' a))
(h : ∀ (s : set β), measurable_set s → ⇑μ' s = ⇑μ (m' ⁻¹' s)) :
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 β ℝ≥0∞)
{f : α → β}
(hf : measurable f) :
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}
theorem
measure_theory.simple_func.measurable_set_support
{α : Type u_1}
{β : Type u_2}
[has_zero β]
[measurable_space α]
(f : measure_theory.simple_func α β) :
@[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.
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) < ⊤
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 α β} :
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) :
@[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) :
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 μ
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 μ
@[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 μ
@[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 μ
@[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 μ
@[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 μ
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 α ℝ≥0∞}
(hm : f.fin_meas_supp μ)
(hf : ∀ᵐ (a : α) ∂μ, ⇑f a ≠ ⊤) :
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 α ℝ≥0∞}
(h : f.lintegral μ ≠ ⊤) :
f.fin_meas_supp μ
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 α ℝ≥0∞}
(hf : ∀ᵐ (a : α) ∂μ, ⇑f a ≠ ⊤) :
f.fin_meas_supp μ ↔ f.lintegral μ < ⊤
@[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)
noncomputable
def
measure_theory.lintegral
{α : Type u_1}
{m : measurable_space α}
(μ : measure_theory.measure α)
(f : α → ℝ≥0∞) :
The lower Lebesgue integral of a function f with respect to a measure μ.
Equations
- measure_theory.lintegral μ f = ⨆ (g : measure_theory.simple_func α ℝ≥0∞) (hf : ⇑g ≤ f), g.lintegral μ
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.simple_func.lintegral_eq_lintegral
{α : Type u_1}
{m : measurable_space α}
(f : measure_theory.simple_func α ℝ≥0∞)
(μ : measure_theory.measure α) :
theorem
measure_theory.lintegral_mono'
{α : Type u_1}
{m : measurable_space α}
⦃μ ν : measure_theory.measure α⦄
(hμν : μ ≤ ν)
⦃f g : α → ℝ≥0∞⦄
(hfg : f ≤ g) :
theorem
measure_theory.lintegral_mono
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
⦃f g : α → ℝ≥0∞⦄
(hfg : f ≤ g) :
theorem
measure_theory.lintegral_mono_nnreal
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → ℝ≥0}
(h : f ≤ g) :
theorem
measure_theory.monotone_lintegral
{α : Type u_1}
{m : measurable_space α}
(μ : measure_theory.measure α) :
@[simp]
theorem
measure_theory.lintegral_const
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(c : ℝ≥0∞) :
@[simp]
theorem
measure_theory.lintegral_one
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α} :
theorem
measure_theory.set_lintegral_const
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(s : set α)
(c : ℝ≥0∞) :
theorem
measure_theory.set_lintegral_one
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(s : set α) :
theorem
measure_theory.lintegral_eq_nnreal
{α : Type u_1}
{m : measurable_space α}
(f : α → ℝ≥0∞)
(μ : measure_theory.measure α) :
∫⁻ a in s, f a ∂μ is defined as the supremum of integrals of simple functions
φ : α →ₛ ℝ≥0∞ such that φ ≤ f. This lemma says that it suffices to take
functions φ : α →ₛ ℝ≥0.
theorem
measure_theory.exists_simple_func_forall_lintegral_sub_lt_of_pos
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ≥0∞}
(h : ∫⁻ (x : α), f x ∂μ ≠ ⊤)
{ε : ℝ≥0∞}
(hε : ε ≠ 0) :
theorem
measure_theory.supr_lintegral_le
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{ι : Sort u_2}
(f : ι → α → ℝ≥0∞) :
theorem
measure_theory.supr2_lintegral_le
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{ι : Sort u_2}
{ι' : ι → Sort u_3}
(f : Π (i : ι), ι' i → α → ℝ≥0∞) :
theorem
measure_theory.le_infi_lintegral
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{ι : Sort u_2}
(f : ι → α → ℝ≥0∞) :
theorem
measure_theory.le_infi2_lintegral
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{ι : Sort u_2}
{ι' : ι → Sort u_3}
(f : Π (i : ι), ι' i → α → ℝ≥0∞) :
theorem
measure_theory.lintegral_mono_ae
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → ℝ≥0∞}
(h : ∀ᵐ (a : α) ∂μ, f a ≤ g a) :
theorem
measure_theory.set_lintegral_mono_ae
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
{f g : α → ℝ≥0∞}
(hf : measurable f)
(hg : measurable g)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x) :
theorem
measure_theory.set_lintegral_mono
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
{f g : α → ℝ≥0∞}
(hf : measurable f)
(hg : measurable g)
(hfg : ∀ (x : α), x ∈ s → f x ≤ g x) :
theorem
measure_theory.lintegral_congr_ae
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → ℝ≥0∞}
(h : f =ᵐ[μ] g) :
theorem
measure_theory.lintegral_congr
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → ℝ≥0∞}
(h : ∀ (a : α), f a = g a) :
theorem
measure_theory.set_lintegral_congr_fun
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → ℝ≥0∞}
{s : set α}
(hs : measurable_set s)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) :
theorem
measure_theory.lintegral_supr
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : ℕ → α → ℝ≥0∞}
(hf : ∀ (n : ℕ), measurable (f n))
(h_mono : monotone f) :
Monotone convergence theorem -- sometimes called Beppo-Levi convergence.
See lintegral_supr_directed for a more general form.
theorem
measure_theory.lintegral_supr'
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : ℕ → α → ℝ≥0∞}
(hf : ∀ (n : ℕ), ae_measurable (f n) μ)
(h_mono : ∀ᵐ (x : α) ∂μ, monotone (λ (n : ℕ), f n x)) :
Monotone convergence theorem -- sometimes called Beppo-Levi convergence. Version with ae_measurable functions.
theorem
measure_theory.lintegral_tendsto_of_tendsto_of_monotone
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : ℕ → α → ℝ≥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}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ≥0∞}
(hf : measurable f) :
theorem
measure_theory.exists_pos_set_lintegral_lt_of_measure_lt
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ≥0∞}
(h : ∫⁻ (x : α), f x ∂μ ≠ ⊤)
{ε : ℝ≥0∞}
(hε : ε ≠ 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. This lemma states states this fact in terms of ε and δ.
theorem
measure_theory.tendsto_set_lintegral_zero
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{ι : Type u_2}
{f : α → ℝ≥0∞}
(h : ∫⁻ (x : α), f x ∂μ ≠ ⊤)
{l : filter ι}
{s : ι → set α}
(hl : filter.tendsto (⇑μ ∘ s) 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}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → ℝ≥0∞}
(hf : measurable f)
(hg : measurable g) :
theorem
measure_theory.lintegral_add'
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → ℝ≥0∞}
(hf : ae_measurable f μ)
(hg : ae_measurable g μ) :
theorem
measure_theory.lintegral_zero
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α} :
theorem
measure_theory.lintegral_zero_fun
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α} :
@[simp]
theorem
measure_theory.lintegral_smul_measure
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(c : ℝ≥0∞)
(f : α → ℝ≥0∞) :
@[simp]
theorem
measure_theory.lintegral_sum_measure
{α : Type u_1}
{m : measurable_space α}
{ι : Type u_2}
(f : α → ℝ≥0∞)
(μ : ι → measure_theory.measure α) :
@[simp]
theorem
measure_theory.lintegral_zero_measure
{α : Type u_1}
{m : measurable_space α}
(f : α → ℝ≥0∞) :
theorem
measure_theory.set_lintegral_empty
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(f : α → ℝ≥0∞) :
theorem
measure_theory.set_lintegral_univ
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(f : α → ℝ≥0∞) :
theorem
measure_theory.set_lintegral_measure_zero
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(s : set α)
(f : α → ℝ≥0∞)
(hs' : ⇑μ s = 0) :
theorem
measure_theory.lintegral_finset_sum
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
(s : finset β)
{f : β → α → ℝ≥0∞}
(hf : ∀ (b : β), b ∈ s → measurable (f b)) :
@[simp]
theorem
measure_theory.lintegral_const_mul
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(r : ℝ≥0∞)
{f : α → ℝ≥0∞}
(hf : measurable f) :
theorem
measure_theory.lintegral_const_mul''
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(r : ℝ≥0∞)
{f : α → ℝ≥0∞}
(hf : ae_measurable f μ) :
theorem
measure_theory.lintegral_const_mul_le
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(r : ℝ≥0∞)
(f : α → ℝ≥0∞) :
theorem
measure_theory.lintegral_mul_const
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(r : ℝ≥0∞)
{f : α → ℝ≥0∞}
(hf : measurable f) :
theorem
measure_theory.lintegral_mul_const''
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(r : ℝ≥0∞)
{f : α → ℝ≥0∞}
(hf : ae_measurable f μ) :
theorem
measure_theory.lintegral_mul_const_le
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(r : ℝ≥0∞)
(f : α → ℝ≥0∞) :
theorem
measure_theory.lintegral_lintegral_mul
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{β : Type u_2}
[measurable_space β]
{ν : measure_theory.measure β}
{f : α → ℝ≥0∞}
{g : β → ℝ≥0∞}
(hf : ae_measurable f μ)
(hg : ae_measurable g ν) :
theorem
measure_theory.lintegral_rw₁
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f f' : α → β}
(h : f =ᵐ[μ] f')
(g : β → ℝ≥0∞) :
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 : β → γ → ℝ≥0∞) :
@[simp]
theorem
measure_theory.lintegral_indicator
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(f : α → ℝ≥0∞)
{s : set α}
(hs : measurable_set s) :
theorem
measure_theory.set_lintegral_eq_const
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ≥0∞}
(hf : measurable f)
(r : ℝ≥0∞) :
theorem
measure_theory.mul_meas_ge_le_lintegral
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ≥0∞}
(hf : measurable f)
(ε : ℝ≥0∞) :
Markov's inequality also known as Chebyshev's first inequality.
theorem
measure_theory.lintegral_eq_top_of_measure_eq_top_pos
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ≥0∞}
(hf : measurable f)
(hμf : 0 < ⇑μ {x : α | f x = ⊤}) :
theorem
measure_theory.meas_ge_le_lintegral_div
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ≥0∞}
(hf : measurable f)
{ε : ℝ≥0∞}
(hε : ε ≠ 0)
(hε' : ε ≠ ⊤) :
@[simp]
theorem
measure_theory.lintegral_eq_zero_iff
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ≥0∞}
(hf : measurable f) :
@[simp]
theorem
measure_theory.lintegral_eq_zero_iff'
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ≥0∞}
(hf : ae_measurable f μ) :
theorem
measure_theory.lintegral_pos_iff_support
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ≥0∞}
(hf : measurable f) :
theorem
measure_theory.lintegral_supr_ae
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : ℕ → α → ℝ≥0∞}
(hf : ∀ (n : ℕ), measurable (f n))
(h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a) :
Weaker version of the monotone convergence theorem
theorem
measure_theory.lintegral_sub_le
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(f g : α → ℝ≥0∞)
(hf : measurable f)
(hg : measurable g)
(h : f ≤ᵐ[μ] g) :
theorem
measure_theory.lintegral_strict_mono_of_ae_le_of_ae_lt_on
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → ℝ≥0∞}
(hf : measurable f)
(hg : measurable g)
(hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤)
(h_le : f ≤ᵐ[μ] g)
{s : set α}
(hμs : ⇑μ s ≠ 0)
(h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x < g x) :
theorem
measure_theory.lintegral_strict_mono
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → ℝ≥0∞}
(hμ : μ ≠ 0)
(hf : measurable f)
(hg : measurable g)
(hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤)
(h : ∀ᵐ (x : α) ∂μ, f x < g x) :
theorem
measure_theory.set_lintegral_strict_mono
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → ℝ≥0∞}
{s : set α}
(hsm : measurable_set s)
(hs : ⇑μ s ≠ 0)
(hf : measurable f)
(hg : measurable g)
(hfi : ∫⁻ (x : α) in s, f x ∂μ ≠ ⊤)
(h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x < g x) :
theorem
measure_theory.lintegral_infi_ae
{α : Type u_1}
{m : measurable_space α}
{μ : 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 ∂μ ≠ ⊤) :
Monotone convergence theorem for nonincreasing sequences of functions
theorem
measure_theory.lintegral_infi
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : ℕ → α → ℝ≥0∞}
(h_meas : ∀ (n : ℕ), measurable (f n))
(h_anti : antitone f)
(h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤) :
Monotone convergence theorem for nonincreasing sequences of functions
theorem
measure_theory.lintegral_liminf_le'
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : ℕ → α → ℝ≥0∞}
(h_meas : ∀ (n : ℕ), ae_measurable (f n) μ) :
Known as Fatou's lemma, version with ae_measurable functions
theorem
measure_theory.lintegral_liminf_le
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : ℕ → α → ℝ≥0∞}
(h_meas : ∀ (n : ℕ), measurable (f n)) :
Known as Fatou's lemma
theorem
measure_theory.limsup_lintegral_le
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : ℕ → α → ℝ≥0∞}
{g : α → ℝ≥0∞}
(hf_meas : ∀ (n : ℕ), measurable (f n))
(h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g)
(h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤) :
theorem
measure_theory.tendsto_lintegral_of_dominated_convergence
{α : Type u_1}
{m : measurable_space α}
{μ : 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}
{m : measurable_space α}
{μ : 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}
{m : measurable_space α}
{μ : measure_theory.measure α}
{ι : Type u_2}
{l : filter ι}
[l.is_countably_generated]
{F : ι → α → ℝ≥0∞}
{f : α → ℝ≥0∞}
(bound : α → ℝ≥0∞)
(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))) :
Dominated convergence theorem for filters with a countable basis
theorem
measure_theory.lintegral_supr_directed
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[encodable β]
{f : β → α → ℝ≥0∞}
(hf : ∀ (b : β), measurable (f b))
(h_directed : directed has_le.le f) :
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}
{m : measurable_space α}
{μ : measure_theory.measure α}
[encodable β]
{f : β → α → ℝ≥0∞}
(hf : ∀ (i : β), measurable (f i)) :
theorem
measure_theory.lintegral_Union
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[encodable β]
{s : β → set α}
(hm : ∀ (i : β), measurable_set (s i))
(hd : pairwise (disjoint on s))
(f : α → ℝ≥0∞) :
theorem
measure_theory.lintegral_union
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ≥0∞}
{A B : set α}
(hA : measurable_set A)
(hB : measurable_set B)
(hAB : disjoint A B) :
theorem
measure_theory.lintegral_map
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[measurable_space β]
{f : β → ℝ≥0∞}
{g : α → β}
(hf : measurable f)
(hg : measurable g) :
theorem
measure_theory.lintegral_map'
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[measurable_space β]
{f : β → ℝ≥0∞}
{g : α → β}
(hf : ae_measurable f (⇑(measure_theory.measure.map g) μ))
(hg : measurable g) :
theorem
measure_theory.lintegral_comp
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[measurable_space β]
{f : β → ℝ≥0∞}
{g : α → β}
(hf : measurable f)
(hg : measurable g) :
measure_theory.lintegral μ (f ∘ g) = ∫⁻ (a : β), f a ∂⇑(measure_theory.measure.map g) μ
theorem
measure_theory.set_lintegral_map
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[measurable_space β]
{f : β → ℝ≥0∞}
{g : α → β}
{s : set β}
(hs : measurable_set s)
(hf : measurable f)
(hg : measurable g) :
theorem
measurable_embedding.lintegral_map
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[measurable_space β]
{g : α → β}
(hg : measurable_embedding g)
(f : β → ℝ≥0∞) :
If g : α → β is a measurable embedding and f : β → ℝ≥0∞ is any function (not necessarily
measurable), then ∫⁻ a, f a ∂(map g μ) = ∫⁻ a, f (g a) ∂μ. Compare with lintegral_map wich
applies to any measurable g : α → β but requires that f is measurable as well.
theorem
measure_theory.lintegral_map_equiv
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[measurable_space β]
(f : β → ℝ≥0∞)
(g : α ≃ᵐ β) :
The lintegral transforms appropriately under a measurable equivalence g : α ≃ᵐ β.
(Compare lintegral_map, which applies to a wider class of functions g : α → β, but requires
measurability of the function being integrated.)
theorem
measure_theory.measure_preserving.lintegral_comp
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{mb : measurable_space β}
{ν : measure_theory.measure β}
{g : α → β}
(hg : measure_theory.measure_preserving g μ ν)
{f : β → ℝ≥0∞}
(hf : measurable f) :
theorem
measure_theory.measure_preserving.lintegral_comp_emb
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{mb : measurable_space β}
{ν : measure_theory.measure β}
{g : α → β}
(hg : measure_theory.measure_preserving g μ ν)
(hge : measurable_embedding g)
(f : β → ℝ≥0∞) :
theorem
measure_theory.measure_preserving.set_lintegral_comp_preimage
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{mb : measurable_space β}
{ν : measure_theory.measure β}
{g : α → β}
(hg : measure_theory.measure_preserving g μ ν)
{s : set β}
(hs : measurable_set s)
{f : β → ℝ≥0∞}
(hf : measurable f) :
theorem
measure_theory.measure_preserving.set_lintegral_comp_preimage_emb
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{mb : measurable_space β}
{ν : measure_theory.measure β}
{g : α → β}
(hg : measure_theory.measure_preserving g μ ν)
(hge : measurable_embedding g)
(f : β → ℝ≥0∞)
(s : set β) :
theorem
measure_theory.measure_preserving.set_lintegral_comp_emb
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{mb : measurable_space β}
{ν : measure_theory.measure β}
{g : α → β}
(hg : measure_theory.measure_preserving g μ ν)
(hge : measurable_embedding g)
(f : β → ℝ≥0∞)
(s : set α) :
theorem
measure_theory.lintegral_dirac'
{α : Type u_1}
[measurable_space α]
(a : α)
{f : α → ℝ≥0∞}
(hf : measurable f) :
∫⁻ (a : α), f a ∂measure_theory.measure.dirac a = f a
theorem
measure_theory.lintegral_dirac
{α : Type u_1}
[measurable_space α]
[measurable_singleton_class α]
(a : α)
(f : α → ℝ≥0∞) :
∫⁻ (a : α), f a ∂measure_theory.measure.dirac a = f a
theorem
measure_theory.lintegral_encodable
{α : Type u_1}
{m : measurable_space α}
[encodable α]
[measurable_singleton_class α]
(f : α → ℝ≥0∞)
(μ : measure_theory.measure α) :
theorem
measure_theory.lintegral_count'
{α : Type u_1}
[measurable_space α]
{f : α → ℝ≥0∞}
(hf : measurable f) :
∫⁻ (a : α), f a ∂measure_theory.measure.count = ∑' (a : α), f a
theorem
measure_theory.lintegral_count
{α : Type u_1}
[measurable_space α]
[measurable_singleton_class α]
(f : α → ℝ≥0∞) :
∫⁻ (a : α), f a ∂measure_theory.measure.count = ∑' (a : α), f a
theorem
measure_theory.ae_lt_top
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ≥0∞}
(hf : measurable f)
(h2f : ∫⁻ (x : α), f x ∂μ ≠ ⊤) :
theorem
measure_theory.ae_lt_top'
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ≥0∞}
(hf : ae_measurable f μ)
(h2f : ∫⁻ (x : α), f x ∂μ ≠ ⊤) :
theorem
measure_theory.set_lintegral_lt_top_of_bdd_above
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hs : ⇑μ s ≠ ⊤)
{f : α → ℝ≥0}
(hf : measurable f)
(hbdd : bdd_above (f '' s)) :
theorem
measure_theory.set_lintegral_lt_top_of_is_compact
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space α]
[opens_measurable_space α]
{s : set α}
(hs : ⇑μ s ≠ ⊤)
(hsc : is_compact s)
{f : α → ℝ≥0}
(hf : continuous f) :
theorem
is_finite_measure.lintegral_lt_top_of_bounded_to_ennreal
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
[μ_fin : measure_theory.is_finite_measure μ]
{f : α → ℝ≥0∞}
(f_bdd : ∃ (c : ℝ≥0), ∀ (x : α), f x ≤ ↑c) :
noncomputable
def
measure_theory.measure.with_density
{α : Type u_1}
{m : measurable_space α}
(μ : 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
- μ.with_density f = measure_theory.measure.of_measurable (λ (s : set α) (hs : measurable_set s), ∫⁻ (a : α) in s, f a ∂μ) _ _
@[simp]
theorem
measure_theory.with_density_apply
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(f : α → ℝ≥0∞)
{s : set α}
(hs : measurable_set s) :
theorem
measure_theory.with_density_add
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → ℝ≥0∞}
(hf : measurable f)
(hg : measurable g) :
μ.with_density (f + g) = μ.with_density f + μ.with_density g
theorem
measure_theory.with_density_smul
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(r : ℝ≥0∞)
{f : α → ℝ≥0∞}
(hf : measurable f) :
μ.with_density (r • f) = r • μ.with_density f
theorem
measure_theory.with_density_smul'
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(r : ℝ≥0∞)
(f : α → ℝ≥0∞)
(hr : r ≠ ⊤) :
μ.with_density (r • f) = r • μ.with_density f
theorem
measure_theory.is_finite_measure_with_density
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ≥0∞}
(hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤) :
theorem
measure_theory.with_density_absolutely_continuous
{α : Type u_1}
{m : measurable_space α}
(μ : measure_theory.measure α)
(f : α → ℝ≥0∞) :
μ.with_density f ≪ μ
@[simp]
theorem
measure_theory.with_density_zero
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α} :
μ.with_density 0 = 0
@[simp]
theorem
measure_theory.with_density_one
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α} :
μ.with_density 1 = μ
theorem
measure_theory.with_density_tsum
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : ℕ → α → ℝ≥0∞}
(h : ∀ (i : ℕ), measurable (f i)) :
μ.with_density (∑' (n : ℕ), f n) = measure_theory.measure.sum (λ (n : ℕ), μ.with_density (f n))
theorem
measure_theory.with_density_indicator
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hs : measurable_set s)
(f : α → ℝ≥0∞) :
μ.with_density (s.indicator f) = (μ.restrict s).with_density f
theorem
measure_theory.with_density_indicator_one
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hs : measurable_set s) :
μ.with_density (s.indicator 1) = μ.restrict s
theorem
measure_theory.with_density_of_real_mutually_singular
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ}
(hf : measurable f) :
μ.with_density (λ (x : α), ennreal.of_real (f x)) ⊥ₘ μ.with_density (λ (x : α), ennreal.of_real (-f x))
theorem
measure_theory.restrict_with_density
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hs : measurable_set s)
(f : α → ℝ≥0∞) :
(μ.with_density f).restrict s = (μ.restrict s).with_density f
theorem
measure_theory.with_density_eq_zero
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ≥0∞}
(hf : ae_measurable f μ)
(h : μ.with_density f = 0) :
theorem
measurable.ennreal_induction
{α : Type u_1}
[measurable_space α]
{P : (α → ℝ≥0∞) → Prop}
(h_ind : ∀ (c : ℝ≥0∞) ⦃s : set α⦄, measurable_set s → P (s.indicator (λ (_x : α), c)))
(h_add : ∀ ⦃f g : α → ℝ≥0∞⦄, disjoint (function.support f) (function.support g) → measurable f → measurable g → P f → P g → P (f + g))
(h_supr : ∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), measurable (f n)) → monotone f → (∀ (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}
{m : measurable_space α}
(μ : measure_theory.measure α)
{f : α → ℝ≥0∞}
(h_mf : measurable f)
{g : α → ℝ≥0∞} :
measurable g → ∫⁻ (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.with_density_mul
{α : Type u_1}
{m : measurable_space α}
(μ : measure_theory.measure α)
{f g : α → ℝ≥0∞}
(hf : measurable f)
(hg : measurable g) :
μ.with_density (f * g) = (μ.with_density f).with_density g
theorem
measure_theory.set_lintegral_with_density_eq_set_lintegral_mul
{α : Type u_1}
{m : measurable_space α}
(μ : measure_theory.measure α)
{f g : α → ℝ≥0∞}
(hf : measurable f)
(hg : measurable g)
{s : set α}
(hs : measurable_set s) :