Lebesgue integral for ennreal-valued functions
We define simple functions and show that each Borel measurable function on ennreal can be
approximated by a sequence of simple functions.
Notation
We introduce the following notation for the lower Lebesgue integral of a function f : α → ennreal.
∫⁻ x, f x ∂μ: integral of a functionf : α → ennrealwith respect to a measureμ;∫⁻ x, f x: integral of a functionf : α → ennrealwith respect to the canonical measurevolumeonα;∫⁻ x in s, f x ∂μ: integral of a functionf : α → ennrealover a setswith respect to a measureμ, defined as∫⁻ x, f x ∂(μ.restrict s);∫⁻ x in s, f x: integral of a functionf : α → ennrealover a setswith respect to the canonical measurevolume, defined as∫⁻ x, f x ∂(volume.restrict s).
- to_fun : α → β
- is_measurable_fiber' : ∀ (x : β), is_measurable (c.to_fun ⁻¹' {x})
- finite_range' : (set.range c.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.
@[instance]
def
measure_theory.simple_func.has_coe_to_fun
{α : Type u_1}
{β : Type u_2}
[measurable_space α] :
Equations
- measure_theory.simple_func.has_coe_to_fun = {F := λ (x : measure_theory.simple_func α β), α → β, coe := measure_theory.simple_func.to_fun β}
theorem
measure_theory.simple_func.coe_injective
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
⦃f g : measure_theory.simple_func α β⦄ :
@[ext]
theorem
measure_theory.simple_func.ext
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{f g : measure_theory.simple_func α β} :
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.is_measurable_fiber
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
(f : measure_theory.simple_func α β)
(x : β) :
is_measurable (⇑f ⁻¹' {x})
def
measure_theory.simple_func.range
{α : Type u_1}
{β : Type u_2}
[measurable_space α] :
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 α} :
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 : β) :
def
measure_theory.simple_func.const
(α : Type u_1)
{β : Type u_2}
[measurable_space α] :
β → measure_theory.simple_func α β
Constant function as a simple_func.
Equations
- measure_theory.simple_func.const α b = {to_fun := λ (a : α), b, is_measurable_fiber' := _, finite_range' := _}
@[instance]
def
measure_theory.simple_func.inhabited
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[inhabited β] :
Equations
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.is_measurable_cut
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
(r : α → β → Prop)
(f : measure_theory.simple_func α β) :
(∀ (b : β), is_measurable {a : α | r a b}) → is_measurable {a : α | r a (⇑f a)}
theorem
measure_theory.simple_func.is_measurable_preimage
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
(f : measure_theory.simple_func α β)
(s : set β) :
is_measurable (⇑f ⁻¹' s)
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
def
measure_theory.simple_func.piecewise
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
(s : set α) :
is_measurable s → measure_theory.simple_func α β → measure_theory.simple_func α β → 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 : α), s.decidable_mem j), is_measurable_fiber' := _, finite_range' := _}
@[simp]
theorem
measure_theory.simple_func.coe_piecewise
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{s : set α}
(hs : is_measurable 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 : is_measurable 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 : is_measurable 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 α β) :
def
measure_theory.simple_func.bind
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α] :
measure_theory.simple_func α β → (β → 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
- f.bind g = {to_fun := λ (a : α), ⇑(g (⇑f a)) a, is_measurable_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 α] :
(β → γ) → 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
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 : α → β) :
measurable g → measure_theory.simple_func α γ
Composition of a simple_fun and a measurable function is a simple_func.
Equations
- f.comp g hgm = {to_fun := ⇑f ∘ g, is_measurable_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) :
def
measure_theory.simple_func.seq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α] :
measure_theory.simple_func α (β → γ) → 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
- 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 α] :
measure_theory.simple_func α β → 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
@[instance]
def
measure_theory.simple_func.has_zero
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_zero β] :
Equations
@[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}
@[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}
@[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}
@[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}
@[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]
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]
theorem
measure_theory.simple_func.coe_add
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_add β]
(f g : measure_theory.simple_func α β) :
@[simp]
theorem
measure_theory.simple_func.coe_mul
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_mul β]
(f g : measure_theory.simple_func α β) :
@[simp]
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 β] :
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
@[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
@[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
@[instance]
def
measure_theory.simple_func.has_neg
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_neg β] :
Equations
@[simp]
theorem
measure_theory.simple_func.coe_neg
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_neg β]
(f : measure_theory.simple_func α β) :
@[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
@[simp]
theorem
measure_theory.simple_func.coe_sub
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[add_group β]
(f g : measure_theory.simple_func α β) :
@[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
@[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 : α) :
@[instance]
def
measure_theory.simple_func.semimodule
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{K : Type u_5}
[semiring K]
[add_comm_monoid β]
[semimodule K β] :
semimodule K (measure_theory.simple_func α β)
Equations
- measure_theory.simple_func.semimodule = function.injective.semimodule 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.semimodule._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
@[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 := _}
@[instance]
def
measure_theory.simple_func.partial_order
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[partial_order β] :
Equations
@[instance]
def
measure_theory.simple_func.order_bot
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[order_bot β] :
Equations
@[instance]
def
measure_theory.simple_func.order_top
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[order_top β] :
Equations
@[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 := _}
@[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 := _}
@[instance]
def
measure_theory.simple_func.semilattice_sup_bot
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[semilattice_sup_bot β] :
Equations
- measure_theory.simple_func.semilattice_sup_bot = {bot := order_bot.bot measure_theory.simple_func.order_bot, 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 := _, bot_le := _, sup := semilattice_sup.sup measure_theory.simple_func.semilattice_sup, le_sup_left := _, le_sup_right := _, sup_le := _}
@[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 := _}
@[instance]
def
measure_theory.simple_func.bounded_lattice
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[bounded_lattice β] :
Equations
- measure_theory.simple_func.bounded_lattice = {sup := lattice.sup measure_theory.simple_func.lattice, le := lattice.le measure_theory.simple_func.lattice, lt := lattice.lt measure_theory.simple_func.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf measure_theory.simple_func.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, top := order_top.top measure_theory.simple_func.order_top, le_top := _, bot := order_bot.bot measure_theory.simple_func.order_bot, bot_le := _}
theorem
measure_theory.simple_func.finset_sup_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
[semilattice_sup_bot β]
{f : γ → measure_theory.simple_func α β}
(s : finset γ)
(a : α) :
def
measure_theory.simple_func.restrict
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_zero β] :
measure_theory.simple_func α β → 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
- f.restrict s = dite (is_measurable s) (λ (hs : is_measurable s), measure_theory.simple_func.piecewise s hs f 0) (λ (hs : ¬is_measurable 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 α} :
¬is_measurable s → f.restrict s = 0
@[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 α} :
@[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 α nnreal)
(s : set α) :
theorem
measure_theory.simple_func.map_coe_nnreal_restrict
{α : Type u_1}
[measurable_space α]
(f : measure_theory.simple_func α nnreal)
(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 : is_measurable 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 : is_measurable s)
{t : set β} :
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 : is_measurable s)
{r : β} :
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 α β} :
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 α β} :
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 α β} :
def
measure_theory.simple_func.approx
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[semilattice_sup_bot β]
[has_zero β] :
(ℕ → β) → (α → β) → ℕ → measure_theory.simple_func α β
Fix a sequence i : ℕ → β. Given a function α → β, its n-th approximation
by simple functions is defined so that in case β = ennreal 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_bot β]
[has_zero β]
[topological_space β]
[order_closed_topology β]
[measurable_space β]
[opens_measurable_space β]
{i : ℕ → β}
{f : α → β}
{n : ℕ}
(a : α) :
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_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_bot β]
[has_zero β]
[topological_space β]
[order_closed_topology β]
[measurable_space β]
[opens_measurable_space β]
[measurable_space γ]
{i : ℕ → β}
{f : γ → β}
{g : α → γ}
{n : ℕ}
(a : α) :
measurable f → 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 : α) :
measurable f → 0 = ⊥ → ((⨆ (n : ℕ), ⇑(measure_theory.simple_func.approx i f n) a) = ⨆ (k : ℕ) (h : i k ≤ f a), i k)
A sequence of ennreals such that its range is the set of non-negative rational numbers.
Equations
def
measure_theory.simple_func.eapprox
{α : Type u_1}
[measurable_space α] :
(α → ennreal) → ℕ → measure_theory.simple_func α ennreal
Approximate a function α → ennreal by a sequence of simple functions.
theorem
measure_theory.simple_func.monotone_eapprox
{α : Type u_1}
[measurable_space α]
(f : α → ennreal) :
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
theorem
measure_theory.simple_func.eapprox_comp
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{f : γ → ennreal}
{g : α → γ}
{n : ℕ} :
measurable f → measurable g → ⇑(measure_theory.simple_func.eapprox (f ∘ g) n) = ⇑(measure_theory.simple_func.eapprox f n) ∘ g
Integral of a simple function whose codomain is ennreal.
theorem
measure_theory.simple_func.lintegral_eq_of_subset
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f : measure_theory.simple_func α ennreal)
{s : finset ennreal} :
theorem
measure_theory.simple_func.map_lintegral
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
(g : β → ennreal)
(f : measure_theory.simple_func α β) :
Calculate the integral of (g ∘ f), where g : β → ennreal and f : α →ₛ β.
theorem
measure_theory.simple_func.add_lintegral
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f g : measure_theory.simple_func α ennreal) :
theorem
measure_theory.simple_func.const_mul_lintegral
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f : measure_theory.simple_func α ennreal)
(x : ennreal) :
Integral of a simple function α →ₛ ennreal as a bilinear map.
@[simp]
theorem
measure_theory.simple_func.zero_lintegral
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
theorem
measure_theory.simple_func.lintegral_add
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
(f : measure_theory.simple_func α ennreal) :
theorem
measure_theory.simple_func.lintegral_smul
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f : measure_theory.simple_func α ennreal)
(c : ennreal) :
@[simp]
theorem
measure_theory.simple_func.lintegral_zero
{α : Type u_1}
[measurable_space α]
(f : measure_theory.simple_func α ennreal) :
theorem
measure_theory.simple_func.lintegral_sum
{α : Type u_1}
[measurable_space α]
{ι : Type u_2}
(f : measure_theory.simple_func α ennreal)
(μ : ι → measure_theory.measure α) :
f.lintegral (measure_theory.measure.sum μ) = ∑' (i : ι), f.lintegral (μ i)
theorem
measure_theory.simple_func.restrict_lintegral
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f : measure_theory.simple_func α ennreal)
{s : set α} :
theorem
measure_theory.simple_func.lintegral_restrict
{α : Type u_1}
[measurable_space α]
(f : measure_theory.simple_func α ennreal)
(s : set α)
(μ : measure_theory.measure α) :
theorem
measure_theory.simple_func.restrict_lintegral_eq_lintegral_restrict
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f : measure_theory.simple_func α ennreal)
{s : set α} :
theorem
measure_theory.simple_func.const_lintegral
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(c : ennreal) :
theorem
measure_theory.simple_func.const_lintegral_restrict
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(c : ennreal)
(s : set α) :
theorem
measure_theory.simple_func.restrict_const_lintegral
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(c : ennreal)
{s : set α} :
is_measurable s → ((measure_theory.simple_func.const α c).restrict s).lintegral μ = c * ⇑μ s
theorem
measure_theory.simple_func.le_sup_lintegral
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f g : measure_theory.simple_func α ennreal) :
theorem
measure_theory.simple_func.lintegral_mono
{α : Type u_1}
[measurable_space α]
{f g : measure_theory.simple_func α ennreal}
(hfg : f ≤ g)
{μ ν : measure_theory.measure α} :
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}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space β]
{f : measure_theory.simple_func α ennreal}
{g : measure_theory.simple_func β ennreal}
{ν : measure_theory.measure β} :
simple_func.lintegral depends only on the measures of f ⁻¹' {y}.
theorem
measure_theory.simple_func.lintegral_congr
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : measure_theory.simple_func α ennreal} :
If two simple functions are equal a.e., then their lintegrals are equal.
theorem
measure_theory.simple_func.lintegral_map
{α : Type u_1}
[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 : α → β) :
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}
def
measure_theory.simple_func.fin_meas_supp
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_zero β] :
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}
[measurable_space α]
[has_zero β]
{f : measure_theory.simple_func α β}
{μ : measure_theory.measure α} :
f.fin_meas_supp μ ↔ ⇑μ (function.support ⇑f) < ⊤
theorem
measure_theory.simple_func.fin_meas_supp_iff
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_zero β]
{f : measure_theory.simple_func α β}
{μ : measure_theory.measure α} :
theorem
measure_theory.simple_func.fin_meas_supp.meas_preimage_singleton_ne_zero
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_zero β]
{μ : measure_theory.measure α}
{f : measure_theory.simple_func α β}
(h : f.fin_meas_supp μ)
{y : β} :
theorem
measure_theory.simple_func.fin_meas_supp.map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
[has_zero β]
[has_zero γ]
{μ : measure_theory.measure α}
{f : measure_theory.simple_func α β}
{g : β → γ} :
f.fin_meas_supp μ → g 0 = 0 → (measure_theory.simple_func.map g f).fin_meas_supp μ
theorem
measure_theory.simple_func.fin_meas_supp.of_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
[has_zero β]
[has_zero γ]
{μ : measure_theory.measure α}
{f : measure_theory.simple_func α β}
{g : β → γ} :
(measure_theory.simple_func.map g f).fin_meas_supp μ → (∀ (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}
[measurable_space α]
[has_zero β]
[has_zero γ]
{μ : measure_theory.measure α}
{f : measure_theory.simple_func α β}
{g : β → γ} :
(∀ {b : β}, g b = 0 ↔ b = 0) → ((measure_theory.simple_func.map g f).fin_meas_supp μ ↔ f.fin_meas_supp μ)
theorem
measure_theory.simple_func.fin_meas_supp.pair
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
[has_zero β]
[has_zero γ]
{μ : measure_theory.measure α}
{f : measure_theory.simple_func α β}
{g : measure_theory.simple_func α γ} :
f.fin_meas_supp μ → g.fin_meas_supp μ → (f.pair g).fin_meas_supp μ
theorem
measure_theory.simple_func.fin_meas_supp.map₂
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[measurable_space α]
[has_zero β]
[has_zero γ]
[has_zero δ]
{μ : measure_theory.measure α}
{f : measure_theory.simple_func α β}
(hf : f.fin_meas_supp μ)
{g : measure_theory.simple_func α γ}
(hg : g.fin_meas_supp μ)
{op : β → γ → δ} :
op 0 0 = 0 → (measure_theory.simple_func.map (function.uncurry op) (f.pair g)).fin_meas_supp μ
theorem
measure_theory.simple_func.fin_meas_supp.add
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type u_2}
[add_monoid β]
{f g : measure_theory.simple_func α β} :
f.fin_meas_supp μ → g.fin_meas_supp μ → (f + g).fin_meas_supp μ
theorem
measure_theory.simple_func.fin_meas_supp.mul
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type u_2}
[monoid_with_zero β]
{f g : measure_theory.simple_func α β} :
f.fin_meas_supp μ → g.fin_meas_supp μ → (f * g).fin_meas_supp μ
theorem
measure_theory.simple_func.fin_meas_supp.lintegral_lt_top
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : measure_theory.simple_func α ennreal} :
theorem
measure_theory.simple_func.fin_meas_supp.of_lintegral_lt_top
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : measure_theory.simple_func α ennreal} :
f.lintegral μ < ⊤ → f.fin_meas_supp μ
theorem
measure_theory.simple_func.fin_meas_supp.iff_lintegral_lt_top
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : measure_theory.simple_func α ennreal} :
def
measure_theory.lintegral
{α : Type u_1}
[measurable_space α] :
measure_theory.measure α → (α → ennreal) → ennreal
The lower Lebesgue integral of a function f with respect to a measure μ.
Equations
- measure_theory.lintegral μ f = ⨆ (g : measure_theory.simple_func α ennreal) (hf : ⇑g ≤ f), g.lintegral μ
theorem
measure_theory.simple_func.lintegral_eq_lintegral
{α : Type u_1}
[measurable_space α]
(f : measure_theory.simple_func α ennreal)
(μ : measure_theory.measure α) :
theorem
measure_theory.lintegral_mono'
{α : Type u_1}
[measurable_space α]
⦃μ ν : measure_theory.measure α⦄
(hμν : μ ≤ ν)
⦃f g : α → ennreal⦄ :
theorem
measure_theory.lintegral_mono
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
⦃f g : α → ennreal⦄ :
theorem
measure_theory.monotone_lintegral
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α) :
@[simp]
theorem
measure_theory.lintegral_const
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(c : ennreal) :
theorem
measure_theory.lintegral_eq_nnreal
{α : Type u_1}
[measurable_space α]
(f : α → ennreal)
(μ : measure_theory.measure α) :
∫⁻ a in s, f a ∂μ is defined as the supremum of integrals of simple functions
φ : α →ₛ ennreal such that φ ≤ f. This lemma says that it suffices to take
functions φ : α →ₛ ℝ≥0.
theorem
measure_theory.supr_lintegral_le
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{ι : Sort u_2}
(f : ι → α → ennreal) :
theorem
measure_theory.supr2_lintegral_le
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{ι : Sort u_2}
{ι' : ι → Sort u_3}
(f : Π (i : ι), ι' i → α → ennreal) :
theorem
measure_theory.le_infi_lintegral
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{ι : Sort u_2}
(f : ι → α → ennreal) :
theorem
measure_theory.le_infi2_lintegral
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{ι : Sort u_2}
{ι' : ι → Sort u_3}
(f : Π (i : ι), ι' i → α → ennreal) :
theorem
measure_theory.lintegral_supr
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : ℕ → α → ennreal} :
Monotone convergence theorem -- sometimes called Beppo-Levi convergence.
See lintegral_supr_directed for a more general form.
theorem
measure_theory.lintegral_eq_supr_eapprox_lintegral
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : α → ennreal} :
measurable f → (∫⁻ (a : α), f a ∂μ = ⨆ (n : ℕ), (measure_theory.simple_func.eapprox f n).lintegral μ)
theorem
measure_theory.lintegral_add
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : α → ennreal} :
theorem
measure_theory.lintegral_zero
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
theorem
measure_theory.lintegral_smul_measure
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(c : ennreal)
(f : α → ennreal) :
theorem
measure_theory.lintegral_sum_measure
{α : Type u_1}
[measurable_space α]
{ι : Type u_2}
(f : α → ennreal)
(μ : ι → measure_theory.measure α) :
@[simp]
theorem
measure_theory.lintegral_zero_measure
{α : Type u_1}
[measurable_space α]
(f : α → ennreal) :
theorem
measure_theory.lintegral_finset_sum
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
(s : finset β)
{f : β → α → ennreal} :
theorem
measure_theory.lintegral_const_mul
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(r : ennreal)
{f : α → ennreal} :
theorem
measure_theory.lintegral_const_mul_le
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(r : ennreal)
(f : α → ennreal) :
theorem
measure_theory.lintegral_mono_ae
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : α → ennreal} :
theorem
measure_theory.lintegral_congr_ae
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : α → ennreal} :
theorem
measure_theory.lintegral_congr
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : α → ennreal} :
theorem
measure_theory.lintegral_rw₁
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
{f f' : α → β}
(h : f =ᵐ[μ] f')
(g : β → ennreal) :
theorem
measure_theory.lintegral_rw₂
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
{f₁ f₁' : α → β}
{f₂ f₂' : α → γ}
(h₁ : f₁ =ᵐ[μ] f₁')
(h₂ : f₂ =ᵐ[μ] f₂')
(g : β → γ → ennreal) :
@[simp]
theorem
measure_theory.lintegral_indicator
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f : α → ennreal)
{s : set α} :
theorem
measure_theory.mul_meas_ge_le_lintegral
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : α → ennreal}
(hf : measurable f)
(ε : ennreal) :
Chebyshev's inequality
theorem
measure_theory.meas_ge_le_lintegral_div
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : α → ennreal}
(hf : measurable f)
{ε : ennreal} :
theorem
measure_theory.lintegral_eq_zero_iff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : α → ennreal} :
theorem
measure_theory.lintegral_supr_ae
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : ℕ → α → ennreal} :
Weaker version of the monotone convergence theorem
theorem
measure_theory.lintegral_infi_ae
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : ℕ → α → ennreal} :
Monotone convergence theorem for nonincreasing sequences of functions
theorem
measure_theory.lintegral_infi
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : ℕ → α → ennreal} :
Monotone convergence theorem for nonincreasing sequences of functions
theorem
measure_theory.lintegral_liminf_le
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : ℕ → α → ennreal} :
(∀ (n : ℕ), measurable (f n)) → ∫⁻ (a : α), filter.at_top.liminf (λ (n : ℕ), f n a) ∂μ ≤ filter.at_top.liminf (λ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)
Known as Fatou's lemma
theorem
measure_theory.limsup_lintegral_le
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : ℕ → α → ennreal}
{g : α → ennreal} :
theorem
measure_theory.tendsto_lintegral_of_dominated_convergence
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{F : ℕ → α → ennreal}
{f : α → ennreal}
(bound : α → ennreal) :
(∀ (n : ℕ), measurable (F n)) → (∀ (n : ℕ), F n ≤ᵐ[μ] bound) → ∫⁻ (a : α), bound a ∂μ < ⊤ → (∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ℕ), F n a) filter.at_top (nhds (f a))) → filter.tendsto (λ (n : ℕ), ∫⁻ (a : α), F n a ∂μ) filter.at_top (nhds (∫⁻ (a : α), f a ∂μ))
Dominated convergence theorem for nonnegative functions
theorem
measure_theory.tendsto_lintegral_filter_of_dominated_convergence
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{ι : Type u_2}
{l : filter ι}
{F : ι → α → ennreal}
{f : α → ennreal}
(bound : α → ennreal) :
l.is_countably_generated → (∀ᶠ (n : ι) in l, measurable (F n)) → (∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) → ∫⁻ (a : α), bound a ∂μ < ⊤ → (∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ι), F n a) l (nhds (f a))) → filter.tendsto (λ (n : ι), ∫⁻ (a : α), F n a ∂μ) l (nhds (∫⁻ (a : α), f a ∂μ))
Dominated convergence theorem for filters with a countable basis
theorem
measure_theory.lintegral_supr_directed
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[encodable β]
{f : β → α → ennreal} :
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}
[measurable_space α]
{μ : measure_theory.measure α}
[encodable β]
{f : β → α → ennreal} :
theorem
measure_theory.lintegral_Union
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[encodable β]
{s : β → set α}
(hm : ∀ (i : β), is_measurable (s i))
(hd : pairwise (disjoint on s))
(f : α → ennreal) :
theorem
measure_theory.lintegral_map
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space β]
{f : β → ennreal}
{g : α → β} :
measurable f → measurable g → ∫⁻ (a : β), f a ∂⇑(measure_theory.measure.map g) μ = ∫⁻ (a : α), f (g a) ∂μ
theorem
measure_theory.lintegral_dirac
{α : Type u_1}
[measurable_space α]
(a : α)
{f : α → ennreal} :
measurable f → ∫⁻ (a : α), f a ∂measure_theory.measure.dirac a = f a
def
measure_theory.measure.with_density
{α : Type u_1}
[measurable_space α] :
measure_theory.measure α → (α → ennreal) → measure_theory.measure α
Given a measure μ : measure α and a function f : α → ennreal, μ.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 : is_measurable s), ∫⁻ (a : α) in s, f a ∂μ) _ _
theorem
measure_theory.with_density_apply
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f : α → ennreal)
{s : set α} :
is_measurable s → ⇑(μ.with_density f) s = ∫⁻ (a : α) in s, f a ∂μ