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 measurevolume
onα
;∫⁻ x in s, f x ∂μ
: integral of a functionf : α → ℝ≥0∞
over a sets
with respect to a measureμ
, defined as∫⁻ x, f x ∂(μ.restrict s)
;∫⁻ x in s, f x
: integral of a functionf : α → ℝ≥0∞
over a sets
with respect to the canonical measurevolume
, defined as∫⁻ x, f x ∂(volume.restrict s)
.
- 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.
Instances for measure_theory.simple_func
- measure_theory.simple_func.has_sizeof_inst
- measure_theory.simple_func.has_coe_to_fun
- measure_theory.simple_func.inhabited
- measure_theory.simple_func.has_one
- measure_theory.simple_func.has_zero
- measure_theory.simple_func.has_mul
- measure_theory.simple_func.has_add
- measure_theory.simple_func.has_div
- measure_theory.simple_func.has_sub
- measure_theory.simple_func.has_inv
- measure_theory.simple_func.has_neg
- measure_theory.simple_func.has_sup
- measure_theory.simple_func.has_inf
- measure_theory.simple_func.has_le
- measure_theory.simple_func.has_smul
- measure_theory.simple_func.has_nat_pow
- measure_theory.simple_func.has_int_pow
- measure_theory.simple_func.add_monoid
- measure_theory.simple_func.add_comm_monoid
- measure_theory.simple_func.add_group
- measure_theory.simple_func.add_comm_group
- measure_theory.simple_func.monoid
- measure_theory.simple_func.comm_monoid
- measure_theory.simple_func.group
- measure_theory.simple_func.comm_group
- measure_theory.simple_func.module
- measure_theory.simple_func.preorder
- measure_theory.simple_func.partial_order
- measure_theory.simple_func.order_bot
- measure_theory.simple_func.order_top
- measure_theory.simple_func.semilattice_inf
- measure_theory.simple_func.semilattice_sup
- measure_theory.simple_func.lattice
- measure_theory.simple_func.bounded_order
Simple function defined on the empty type.
Equations
- measure_theory.simple_func.of_is_empty = {to_fun := is_empty_elim (λ (a : α), β), measurable_set_fiber' := _, finite_range' := _}
Range of a simple function α →ₛ β
as a finset β
.
Constant function as a simple_func
.
Equations
- measure_theory.simple_func.const α b = {to_fun := λ (a : α), b, measurable_set_fiber' := _, finite_range' := _}
A simple function is measurable
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' := _}
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' := _}
Given a function g : β → γ
and a simple function f : α →ₛ β
, f.map g
return the simple
function g ∘ f : α →ₛ γ
Equations
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' := _}
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' := _}
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)
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
Equations
Equations
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}
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}
Equations
- measure_theory.simple_func.has_div = {div := λ (f g : measure_theory.simple_func α β), (measure_theory.simple_func.map has_div.div f).seq g}
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}
Equations
Equations
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}
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}
Equations
- measure_theory.simple_func.has_le = {le := λ (f g : measure_theory.simple_func α β), ∀ (a : α), ⇑f a ≤ ⇑g a}
Equations
- measure_theory.simple_func.has_smul = {smul := λ (k : K) (f : measure_theory.simple_func α β), measure_theory.simple_func.map (has_smul.smul k) f}
Equations
- measure_theory.simple_func.has_nat_pow = {pow := λ (f : measure_theory.simple_func α β) (n : ℕ), measure_theory.simple_func.map (λ (_x : β), _x ^ n) f}
Equations
- measure_theory.simple_func.has_int_pow = {pow := λ (f : measure_theory.simple_func α β) (n : ℤ), measure_theory.simple_func.map (λ (_x : β), _x ^ n) f}
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 measure_theory.simple_func.add_monoid._proof_3
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 measure_theory.simple_func.add_comm_monoid._proof_3
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 measure_theory.simple_func.add_group._proof_5 measure_theory.simple_func.add_group._proof_6
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 measure_theory.simple_func.add_comm_group._proof_5 measure_theory.simple_func.add_comm_group._proof_6
Equations
- measure_theory.simple_func.monoid = function.injective.monoid (λ (f : measure_theory.simple_func α β), show α → β, from ⇑f) measure_theory.simple_func.coe_injective measure_theory.simple_func.monoid._proof_1 measure_theory.simple_func.monoid._proof_2 measure_theory.simple_func.coe_pow
Equations
- measure_theory.simple_func.comm_monoid = function.injective.comm_monoid (λ (f : measure_theory.simple_func α β), show α → β, from ⇑f) measure_theory.simple_func.coe_injective measure_theory.simple_func.comm_monoid._proof_1 measure_theory.simple_func.comm_monoid._proof_2 measure_theory.simple_func.comm_monoid._proof_3
Equations
- measure_theory.simple_func.group = function.injective.group (λ (f : measure_theory.simple_func α β), show α → β, from ⇑f) measure_theory.simple_func.coe_injective measure_theory.simple_func.group._proof_1 measure_theory.simple_func.group._proof_2 measure_theory.simple_func.group._proof_3 measure_theory.simple_func.group._proof_4 measure_theory.simple_func.group._proof_5 measure_theory.simple_func.group._proof_6
Equations
- measure_theory.simple_func.comm_group = function.injective.comm_group (λ (f : measure_theory.simple_func α β), show α → β, from ⇑f) measure_theory.simple_func.coe_injective measure_theory.simple_func.comm_group._proof_1 measure_theory.simple_func.comm_group._proof_2 measure_theory.simple_func.comm_group._proof_3 measure_theory.simple_func.comm_group._proof_4 measure_theory.simple_func.comm_group._proof_5 measure_theory.simple_func.comm_group._proof_6
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
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 := _}
Equations
Equations
Equations
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 := _}
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 := _}
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 := _}
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)
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})
A sequence of ℝ≥0∞
s such that its range is the set of non-negative rational numbers.
Equations
Approximate a function α → ℝ≥0∞
by a sequence of simple functions.
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)
Integral of a simple function whose codomain is ℝ≥0∞
.
Calculate the integral of (g ∘ f)
, where g : β → ℝ≥0∞
and f : α →ₛ β
.
Integral of a simple function α →ₛ ℝ≥0∞
as a bilinear map.
simple_func.lintegral
is monotone both in function and in measure.
simple_func.lintegral
depends only on the measures of f ⁻¹' {y}
.
If two simple functions are equal a.e., then their lintegral
s are equal.
A simple_func
has finite measure support if it is equal to 0
outside of a set of finite
measure.
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
)
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 μ
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.
For any function f : α → ℝ≥0∞
, there exists a measurable function g ≤ f
with the same
integral.
∫⁻ 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
.
Monotone convergence theorem -- sometimes called Beppo-Levi convergence.
See lintegral_supr_directed
for a more general form.
Monotone convergence theorem -- sometimes called Beppo-Levi convergence. Version with ae_measurable functions.
Monotone convergence theorem expressed with limits
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 δ
.
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.
The sum of the lower Lebesgue integrals of two functions is less than or equal to the integral of their sum. The other inequality needs one of these functions to be (a.e.-)measurable.
If f g : α → ℝ≥0∞
are two functions and one of them is (a.e.) measurable, then the Lebesgue
integral of f + g
equals the sum of integrals. This lemma assumes that f
is integrable, see also
measure_theory.lintegral_add_right
and primed versions of these lemmas.
If f g : α → ℝ≥0∞
are two functions and one of them is (a.e.) measurable, then the Lebesgue
integral of f + g
equals the sum of integrals. This lemma assumes that g
is integrable, see also
measure_theory.lintegral_add_left
and primed versions of these lemmas.