Try doing some basic maths questions in the Lean Theorem Prover. Functions, real numbers, equivalence relations and groups. Click on README.md and then on "Open in CoCalc with one click".
License: APACHE
/-
Copyright (c) 2018 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Johannes Hölzl
Lebesgue integral on `ennreal`.
We define simple functions and show that each Borel measurable function on `ennreal` can be
approximated by a sequence of simple functions.
-/
import
algebra.pi_instances
measure_theory.measure_space
measure_theory.borel_space
noncomputable theory
open lattice set filter
open_locale classical topological_space
namespace measure_theory
variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
/-- 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. -/
structure {u v} simple_func (α : Type u) [measurable_space α] (β : Type v) :=
(to_fun : α → β)
(measurable_sn : ∀ x, is_measurable (to_fun ⁻¹' {x}))
(finite : (set.range to_fun).finite)
local infixr ` →ₛ `:25 := simple_func
namespace simple_func
section measurable
variables [measurable_space α]
instance has_coe_to_fun : has_coe_to_fun (α →ₛ β) := ⟨_, to_fun⟩
@[ext] theorem ext {f g : α →ₛ β} (H : ∀ a, f a = g a) : f = g :=
by cases f; cases g; congr; exact funext H
/-- Range of a simple function `α →ₛ β` as a `finset β`. -/
protected def range (f : α →ₛ β) : finset β := f.finite.to_finset
@[simp] theorem mem_range {f : α →ₛ β} {b} : b ∈ f.range ↔ ∃ a, f a = b :=
finite.mem_to_finset
lemma preimage_eq_empty_iff (f : α →ₛ β) (b : β) : f ⁻¹' {b} = ∅ ↔ b ∉ f.range :=
iff.intro
(by simp [set.eq_empty_iff_forall_not_mem, mem_range])
(by simp [set.eq_empty_iff_forall_not_mem, mem_range])
/-- Constant function as a `simple_func`. -/
def const (α) {β} [measurable_space α] (b : β) : α →ₛ β :=
⟨λ a, b, λ x, is_measurable.const _,
finite_subset (set.finite_singleton b) $ by rintro _ ⟨a, rfl⟩; simp⟩
instance [inhabited β] : inhabited (α →ₛ β) := ⟨const _ (default _)⟩
@[simp] theorem const_apply (a : α) (b : β) : (const α b) a = b := rfl
lemma range_const (α) [measurable_space α] [ne : nonempty α] (b : β) :
(const α b).range = {b} :=
begin
ext b',
simp [mem_range],
exact ⟨assume ⟨_, h⟩, h.symm, assume h, ne.elim $ λa, ⟨a, h.symm⟩⟩
end
lemma is_measurable_cut (p : α → β → Prop) (f : α →ₛ β)
(h : ∀b, is_measurable {a | p a b}) : is_measurable {a | p a (f a)} :=
begin
rw (_ : {a | p a (f a)} = ⋃ b ∈ set.range f, {a | p a b} ∩ f ⁻¹' {b}),
{ exact is_measurable.bUnion (countable_finite f.finite)
(λ b _, is_measurable.inter (h b) (f.measurable_sn _)) },
ext a, simp,
exact ⟨λ h, ⟨_, ⟨a, rfl⟩, h, rfl⟩, λ ⟨_, ⟨a', rfl⟩, h', e⟩, e.symm ▸ h'⟩
end
theorem preimage_measurable (f : α →ₛ β) (s) : is_measurable (f ⁻¹' s) :=
is_measurable_cut (λ _ b, b ∈ s) f (λ b, by simp [is_measurable.const])
/-- A simple function is measurable -/
theorem measurable [measurable_space β] (f : α →ₛ β) : measurable f :=
λ s _, preimage_measurable f s
def ite {s : set α} (hs : is_measurable s) (f g : α →ₛ β) : α →ₛ β :=
⟨λ a, if a ∈ s then f a else g a,
λ x, by letI : measurable_space β := ⊤; exact
measurable.if hs f.measurable g.measurable _ trivial,
finite_subset (finite_union f.finite g.finite) begin
rintro _ ⟨a, rfl⟩,
by_cases a ∈ s; simp [h],
exacts [or.inl ⟨_, rfl⟩, or.inr ⟨_, rfl⟩]
end⟩
@[simp] theorem ite_apply {s : set α} (hs : is_measurable s)
(f g : α →ₛ β) (a) : ite hs f g a = if a ∈ s then f a else g a := rfl
/-- 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`. -/
def bind (f : α →ₛ β) (g : β → α →ₛ γ) : α →ₛ γ :=
⟨λa, g (f a) a,
λ c, is_measurable_cut (λa b, g b a ∈ ({c} : set γ)) f (λ b, (g b).measurable_sn c),
finite_subset (finite_bUnion f.finite (λ b, (g b).finite)) $
by rintro _ ⟨a, rfl⟩; simp; exact ⟨_, ⟨a, rfl⟩, _, rfl⟩⟩
@[simp] theorem bind_apply (f : α →ₛ β) (g : β → α →ₛ γ) (a) :
f.bind g a = g (f a) a := rfl
/-- 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`. -/
def restrict [has_zero β] (f : α →ₛ β) (s : set α) : α →ₛ β :=
if hs : is_measurable s then ite hs f (const α 0) else const α 0
@[simp] theorem restrict_apply [has_zero β]
(f : α →ₛ β) {s : set α} (hs : is_measurable s) (a) :
restrict f s a = if a ∈ s then f a else 0 :=
by unfold_coes; simp [restrict, hs]; apply ite_apply hs
theorem restrict_preimage [has_zero β]
(f : α →ₛ β) {s : set α} (hs : is_measurable s)
{t : set β} (ht : (0:β) ∉ t) : restrict f s ⁻¹' t = s ∩ f ⁻¹' t :=
by ext a; dsimp [preimage]; rw [restrict_apply]; by_cases a ∈ s; simp [h, hs, ht]
/-- Given a function `g : β → γ` and a simple function `f : α →ₛ β`, `f.map g` return the simple
function `g ∘ f : α →ₛ γ` -/
def map (g : β → γ) (f : α →ₛ β) : α →ₛ γ := bind f (const α ∘ g)
@[simp] theorem map_apply (g : β → γ) (f : α →ₛ β) (a) : f.map g a = g (f a) := rfl
theorem map_map (g : β → γ) (h: γ → δ) (f : α →ₛ β) : (f.map g).map h = f.map (h ∘ g) := rfl
theorem coe_map (g : β → γ) (f : α →ₛ β) : (f.map g : α → γ) = g ∘ f := rfl
@[simp] theorem range_map [decidable_eq γ] (g : β → γ) (f : α →ₛ β) :
(f.map g).range = f.range.image g :=
begin
ext c,
simp only [mem_range, exists_prop, mem_range, finset.mem_image, map_apply],
split,
{ rintros ⟨a, rfl⟩, exact ⟨f a, ⟨_, rfl⟩, rfl⟩ },
{ rintros ⟨_, ⟨a, rfl⟩, rfl⟩, exact ⟨_, rfl⟩ }
end
lemma map_preimage (f : α →ₛ β) (g : β → γ) (s : set γ) :
(f.map g) ⁻¹' s = (⋃b∈f.range.filter (λb, g b ∈ s), f ⁻¹' {b}) :=
begin
/- True because `f` only takes finitely many values. -/
ext a',
simp only [mem_Union, set.mem_preimage, exists_prop, set.mem_preimage, map_apply,
finset.mem_filter, mem_range, mem_singleton_iff, exists_eq_right'],
split,
{ assume eq, exact ⟨⟨_, rfl⟩, eq⟩ },
{ rintros ⟨_, eq⟩, exact eq }
end
lemma map_preimage_singleton (f : α →ₛ β) (g : β → γ) (c : γ) :
(f.map g) ⁻¹' {c} = (⋃b∈f.range.filter (λb, g b = c), f ⁻¹' {b}) :=
begin
rw map_preimage,
have : (λb, g b = c) = λb, g b ∈ _root_.singleton c,
funext, rw [eq_iff_iff, mem_singleton_iff],
rw this
end
/-- 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)`. -/
def seq (f : α →ₛ (β → γ)) (g : α →ₛ β) : α →ₛ γ := f.bind (λf, g.map f)
@[simp] lemma seq_apply (f : α →ₛ (β → γ)) (g : α →ₛ β) (a : α) : f.seq g a = f a (g a) := rfl
/-- Combine two simple functions `f : α →ₛ β` and `g : α →ₛ β`
into `λ a, (f a, g a)`. -/
def pair (f : α →ₛ β) (g : α →ₛ γ) : α →ₛ (β × γ) := (f.map prod.mk).seq g
@[simp] lemma pair_apply (f : α →ₛ β) (g : α →ₛ γ) (a) : pair f g a = (f a, g a) := rfl
lemma pair_preimage (f : α →ₛ β) (g : α →ₛ γ) (s : set β) (t : set γ) :
(pair f g) ⁻¹' (set.prod s t) = (f ⁻¹' s) ∩ (g ⁻¹' t) := rfl
/- A special form of `pair_preimage` -/
lemma pair_preimage_singleton (f : α →ₛ β) (g : α →ₛ γ) (b : β) (c : γ) :
(pair f g) ⁻¹' {(b, c)} = (f ⁻¹' {b}) ∩ (g ⁻¹' {c}) :=
by { rw ← prod_singleton_singleton, exact pair_preimage _ _ _ _ }
theorem bind_const (f : α →ₛ β) : f.bind (const α) = f := by ext; simp
instance [has_zero β] : has_zero (α →ₛ β) := ⟨const α 0⟩
instance [has_add β] : has_add (α →ₛ β) := ⟨λf g, (f.map (+)).seq g⟩
instance [has_mul β] : has_mul (α →ₛ β) := ⟨λf g, (f.map (*)).seq g⟩
instance [has_sup β] : has_sup (α →ₛ β) := ⟨λf g, (f.map (⊔)).seq g⟩
instance [has_inf β] : has_inf (α →ₛ β) := ⟨λf g, (f.map (⊓)).seq g⟩
instance [has_le β] : has_le (α →ₛ β) := ⟨λf g, ∀a, f a ≤ g a⟩
@[simp] lemma sup_apply [has_sup β] (f g : α →ₛ β) (a : α) : (f ⊔ g) a = f a ⊔ g a := rfl
@[simp] lemma mul_apply [has_mul β] (f g : α →ₛ β) (a : α) : (f * g) a = f a * g a := rfl
lemma add_apply [has_add β] (f g : α →ₛ β) (a : α) : (f + g) a = f a + g a := rfl
lemma add_eq_map₂ [has_add β] (f g : α →ₛ β) : f + g = (pair f g).map (λp:β×β, p.1 + p.2) :=
rfl
lemma sup_eq_map₂ [has_sup β] (f g : α →ₛ β) : f ⊔ g = (pair f g).map (λp:β×β, p.1 ⊔ p.2) :=
rfl
lemma const_mul_eq_map [has_mul β] (f : α →ₛ β) (b : β) : const α b * f = f.map (λa, b * a) := rfl
instance [add_monoid β] : add_monoid (α →ₛ β) :=
{ add := (+), zero := 0,
add_assoc := assume f g h, ext (assume a, add_assoc _ _ _),
zero_add := assume f, ext (assume a, zero_add _),
add_zero := assume f, ext (assume a, add_zero _) }
instance add_comm_monoid [add_comm_monoid β] : add_comm_monoid (α →ₛ β) :=
{ add_comm := λ f g, ext (λa, add_comm _ _),
.. simple_func.add_monoid }
instance [has_neg β] : has_neg (α →ₛ β) := ⟨λf, f.map (has_neg.neg)⟩
instance [add_group β] : add_group (α →ₛ β) :=
{ neg := has_neg.neg,
add_left_neg := λf, ext (λa, add_left_neg _),
.. simple_func.add_monoid }
instance [add_comm_group β] : add_comm_group (α →ₛ β) :=
{ add_comm := λ f g, ext (λa, add_comm _ _) ,
.. simple_func.add_group }
variables {K : Type*}
instance [has_scalar K β] : has_scalar K (α →ₛ β) := ⟨λk f, f.map (λb, k • b)⟩
instance [semiring K] [add_comm_monoid β] [semimodule K β] : semimodule K (α →ₛ β) :=
{ one_smul := λ f, ext (λa, one_smul _ _),
mul_smul := λ x y f, ext (λa, mul_smul _ _ _),
smul_add := λ r f g, ext (λa, smul_add _ _ _),
smul_zero := λ r, ext (λa, smul_zero _),
add_smul := λ r s f, ext (λa, add_smul _ _ _),
zero_smul := λ f, ext (λa, zero_smul _ _) }
instance [ring K] [add_comm_group β] [module K β] : module K (α →ₛ β) :=
{ .. simple_func.semimodule }
instance [discrete_field K] [add_comm_group β] [module K β] : vector_space K (α →ₛ β) :=
{ .. simple_func.module }
lemma smul_apply [has_scalar K β] (k : K) (f : α →ₛ β) (a : α) : (k • f) a = k • f a := rfl
lemma smul_eq_map [has_scalar K β] (k : K) (f : α →ₛ β) : k • f = f.map (λb, k • b) := rfl
instance [preorder β] : preorder (α →ₛ β) :=
{ le_refl := λf a, le_refl _,
le_trans := λf g h hfg hgh a, le_trans (hfg _) (hgh a),
.. simple_func.has_le }
instance [partial_order β] : partial_order (α →ₛ β) :=
{ le_antisymm := assume f g hfg hgf, ext $ assume a, le_antisymm (hfg a) (hgf a),
.. simple_func.preorder }
instance [order_bot β] : order_bot (α →ₛ β) :=
{ bot := const α ⊥, bot_le := λf a, bot_le, .. simple_func.partial_order }
instance [order_top β] : order_top (α →ₛ β) :=
{ top := const α⊤, le_top := λf a, le_top, .. simple_func.partial_order }
instance [semilattice_inf β] : semilattice_inf (α →ₛ β) :=
{ inf := (⊓),
inf_le_left := assume f g a, inf_le_left,
inf_le_right := assume f g a, inf_le_right,
le_inf := assume f g h hfh hgh a, le_inf (hfh a) (hgh a),
.. simple_func.partial_order }
instance [semilattice_sup β] : semilattice_sup (α →ₛ β) :=
{ sup := (⊔),
le_sup_left := assume f g a, le_sup_left,
le_sup_right := assume f g a, le_sup_right,
sup_le := assume f g h hfh hgh a, sup_le (hfh a) (hgh a),
.. simple_func.partial_order }
instance [semilattice_sup_bot β] : semilattice_sup_bot (α →ₛ β) :=
{ .. simple_func.lattice.semilattice_sup,.. simple_func.lattice.order_bot }
instance [lattice β] : lattice (α →ₛ β) :=
{ .. simple_func.lattice.semilattice_sup,.. simple_func.lattice.semilattice_inf }
instance [bounded_lattice β] : bounded_lattice (α →ₛ β) :=
{ .. simple_func.lattice.lattice, .. simple_func.lattice.order_bot, .. simple_func.lattice.order_top }
lemma finset_sup_apply [semilattice_sup_bot β] {f : γ → α →ₛ β} (s : finset γ) (a : α) :
s.sup f a = s.sup (λc, f c a) :=
begin
refine finset.induction_on s rfl _,
assume a s hs ih,
rw [finset.sup_insert, finset.sup_insert, sup_apply, ih]
end
section approx
section
variables [semilattice_sup_bot β] [has_zero β]
/-- 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. -/
def approx (i : ℕ → β) (f : α → β) (n : ℕ) : α →ₛ β :=
(finset.range n).sup (λk, restrict (const α (i k)) {a:α | i k ≤ f a})
lemma approx_apply [topological_space β] [order_closed_topology β] {i : ℕ → β} {f : α → β} {n : ℕ}
(a : α) (hf : _root_.measurable f) :
(approx i f n : α →ₛ β) a = (finset.range n).sup (λk, if i k ≤ f a then i k else 0) :=
begin
dsimp only [approx],
rw [finset_sup_apply],
congr,
funext k,
rw [restrict_apply],
refl,
exact (hf.preimage $ is_measurable_of_is_closed $ is_closed_ge' _)
end
lemma monotone_approx (i : ℕ → β) (f : α → β) : monotone (approx i f) :=
assume n m h, finset.sup_mono $ finset.range_subset.2 h
lemma approx_comp [topological_space β] [order_closed_topology β] [measurable_space γ]
{i : ℕ → β} {f : γ → β} {g : α → γ} {n : ℕ} (a : α)
(hf : _root_.measurable f) (hg : _root_.measurable g) :
(approx i (f ∘ g) n : α →ₛ β) a = (approx i f n : γ →ₛ β) (g a) :=
by rw [approx_apply _ hf, approx_apply _ (hf.comp hg)]
end
lemma supr_approx_apply [topological_space β] [complete_lattice β] [order_closed_topology β] [has_zero β]
(i : ℕ → β) (f : α → β) (a : α) (hf : _root_.measurable f) (h_zero : (0 : β) = ⊥) :
(⨆n, (approx i f n : α →ₛ β) a) = (⨆k (h : i k ≤ f a), i k) :=
begin
refine le_antisymm (supr_le $ assume n, _) (supr_le $ assume k, supr_le $ assume hk, _),
{ rw [approx_apply a hf, h_zero],
refine finset.sup_le (assume k hk, _),
split_ifs,
exact le_supr_of_le k (le_supr _ h),
exact bot_le },
{ refine le_supr_of_le (k+1) _,
rw [approx_apply a hf],
have : k ∈ finset.range (k+1) := finset.mem_range.2 (nat.lt_succ_self _),
refine le_trans (le_of_eq _) (finset.le_sup this),
rw [if_pos hk] }
end
end approx
section eapprox
/-- A sequence of `ennreal`s such that its range is the set of non-negative rational numbers. -/
def ennreal_rat_embed (n : ℕ) : ennreal :=
nnreal.of_real ((encodable.decode ℚ n).get_or_else (0 : ℚ))
lemma ennreal_rat_embed_encode (q : ℚ) :
ennreal_rat_embed (encodable.encode q) = nnreal.of_real q :=
by rw [ennreal_rat_embed, encodable.encodek]; refl
def eapprox : (α → ennreal) → ℕ → α →ₛ ennreal :=
approx ennreal_rat_embed
lemma monotone_eapprox (f : α → ennreal) : monotone (eapprox f) :=
monotone_approx _ f
lemma supr_eapprox_apply (f : α → ennreal) (hf : _root_.measurable f) (a : α) :
(⨆n, (eapprox f n : α →ₛ ennreal) a) = f a :=
begin
rw [eapprox, supr_approx_apply ennreal_rat_embed f a hf rfl],
refine le_antisymm (supr_le $ assume i, supr_le $ assume hi, hi) (le_of_not_gt _),
assume h,
rcases ennreal.lt_iff_exists_rat_btwn.1 h with ⟨q, hq, lt_q, q_lt⟩,
have : (nnreal.of_real q : ennreal) ≤
(⨆ (k : ℕ) (h : ennreal_rat_embed k ≤ f a), ennreal_rat_embed k),
{ refine le_supr_of_le (encodable.encode q) _,
rw [ennreal_rat_embed_encode q],
refine le_supr_of_le (le_of_lt q_lt) _,
exact le_refl _ },
exact lt_irrefl _ (lt_of_le_of_lt this lt_q)
end
lemma eapprox_comp [measurable_space γ] {f : γ → ennreal} {g : α → γ} {n : ℕ}
(hf : _root_.measurable f) (hg : _root_.measurable g) :
(eapprox (f ∘ g) n : α → ennreal) = (eapprox f n : γ →ₛ ennreal) ∘ g :=
funext $ assume a, approx_comp a hf hg
end eapprox
end measurable
section measure
variables [measure_space α]
lemma volume_bUnion_preimage (s : finset β) (f : α →ₛ β) :
volume (⋃b ∈ s, f ⁻¹' {b}) = s.sum (λb, volume (f ⁻¹' {b})) :=
begin
/- Taking advantage of the fact that `f ⁻¹' {b}` are disjoint for `b ∈ s`. -/
rw [volume_bUnion_finset],
{ simp only [pairwise_on, (on), finset.mem_coe, ne.def],
rintros _ _ _ _ ne _ ⟨h₁, h₂⟩,
simp only [mem_singleton_iff, mem_preimage] at h₁ h₂,
rw [← h₁, h₂] at ne,
exact ne rfl },
exact assume a ha, preimage_measurable _ _
end
/-- Integral of a simple function whose codomain is `ennreal`. -/
def integral (f : α →ₛ ennreal) : ennreal :=
f.range.sum (λ x, x * volume (f ⁻¹' {x}))
/-- Calculate the integral of `(g ∘ f)`, where `g : β → ennreal` and `f : α →ₛ β`. -/
lemma map_integral (g : β → ennreal) (f : α →ₛ β) :
(f.map g).integral = f.range.sum (λ x, g x * volume (f ⁻¹' {x})) :=
begin
simp only [integral, range_map],
refine finset.sum_image' _ (assume b hb, _),
rcases mem_range.1 hb with ⟨a, rfl⟩,
rw [map_preimage_singleton, volume_bUnion_preimage, finset.mul_sum],
refine finset.sum_congr _ _,
{ congr },
{ assume x, simp only [finset.mem_filter], rintro ⟨_, h⟩, rw h }
end
lemma zero_integral : (0 : α →ₛ ennreal).integral = 0 :=
begin
refine (finset.sum_eq_zero_iff_of_nonneg $ assume _ _, zero_le _).2 _,
assume r hr, rcases mem_range.1 hr with ⟨a, rfl⟩,
exact zero_mul _
end
lemma add_integral (f g : α →ₛ ennreal) : (f + g).integral = f.integral + g.integral :=
calc (f + g).integral =
(pair f g).range.sum (λx, x.1 * volume (pair f g ⁻¹' {x}) + x.2 * volume (pair f g ⁻¹' {x})) :
by rw [add_eq_map₂, map_integral]; exact finset.sum_congr rfl (assume a ha, add_mul _ _ _)
... = (pair f g).range.sum (λx, x.1 * volume (pair f g ⁻¹' {x})) +
(pair f g).range.sum (λx, x.2 * volume (pair f g ⁻¹' {x})) : by rw [finset.sum_add_distrib]
... = ((pair f g).map prod.fst).integral + ((pair f g).map prod.snd).integral :
by rw [map_integral, map_integral]
... = integral f + integral g : rfl
lemma const_mul_integral (f : α →ₛ ennreal) (x : ennreal) :
(const α x * f).integral = x * f.integral :=
calc (f.map (λa, x * a)).integral = f.range.sum (λr, x * r * volume (f ⁻¹' {r})) :
by rw [map_integral]
... = f.range.sum (λr, x * (r * volume (f ⁻¹' {r}))) :
finset.sum_congr rfl (assume a ha, mul_assoc _ _ _)
... = x * f.integral :
finset.mul_sum.symm
lemma mem_restrict_range [has_zero β] {r : β} {s : set α} {f : α →ₛ β} (hs : is_measurable s) :
r ∈ (restrict f s).range ↔ (r = 0 ∧ s ≠ univ) ∨ (∃a∈s, f a = r) :=
begin
simp only [mem_range, restrict_apply, hs],
split,
{ rintros ⟨a, ha⟩,
split_ifs at ha,
{ exact or.inr ⟨a, h, ha⟩ },
{ exact or.inl ⟨ha.symm, assume eq, h $ eq.symm ▸ trivial⟩ } },
{ rintros (⟨rfl, h⟩ | ⟨a, ha, rfl⟩),
{ have : ¬ ∀a, a ∈ s := assume this, h $ eq_univ_of_forall this,
rcases not_forall.1 this with ⟨a, ha⟩,
refine ⟨a, _⟩,
rw [if_neg ha] },
{ refine ⟨a, _⟩,
rw [if_pos ha] } }
end
lemma restrict_preimage' {r : ennreal} {s : set α}
(f : α →ₛ ennreal) (hs : is_measurable s) (hr : r ≠ 0) :
(restrict f s) ⁻¹' {r} = (f ⁻¹' {r} ∩ s) :=
begin
ext a,
by_cases a ∈ s; simp [hs, h, hr.symm]
end
lemma restrict_integral (f : α →ₛ ennreal) (s : set α) (hs : is_measurable s) :
(restrict f s).integral = f.range.sum (λr, r * volume (f ⁻¹' {r} ∩ s)) :=
begin
refine finset.sum_bij_ne_zero (λr _ _, r) _ _ _ _,
{ assume r hr,
rcases (mem_restrict_range hs).1 hr with ⟨rfl, h⟩ | ⟨a, ha, rfl⟩,
{ simp },
{ assume _, exact mem_range.2 ⟨a, rfl⟩ } },
{ assume a b _ _ _ _ h, exact h },
{ assume r hr,
by_cases r0 : r = 0, { simp [r0] },
assume h0,
rcases mem_range.1 hr with ⟨a, rfl⟩,
have : f ⁻¹' {f a} ∩ s ≠ ∅,
{ assume h, simpa [h] using h0 },
rcases ne_empty_iff_nonempty.1 this with ⟨a', eq', ha'⟩,
refine ⟨_, (mem_restrict_range hs).2 (or.inr ⟨a', ha', _⟩), _, rfl⟩,
{ simpa using eq' },
{ rwa [restrict_preimage' _ hs r0] } },
{ assume r hr ne,
by_cases r = 0, { simp [h] },
rw [restrict_preimage' _ hs h] }
end
lemma restrict_const_integral (c : ennreal) (s : set α) (hs : is_measurable s) :
(restrict (const α c) s).integral = c * volume s :=
have (@const α ennreal _ c) ⁻¹' {c} = univ,
begin
refine eq_univ_of_forall (assume a, _),
simp,
end,
calc (restrict (const α c) s).integral = c * volume ((const α c) ⁻¹' {c} ∩ s) :
begin
rw [restrict_integral (const α c) s hs],
refine finset.sum_eq_single c _ _,
{ assume r hr, rcases mem_range.1 hr with ⟨a, rfl⟩, contradiction },
{ by_cases nonempty α,
{ assume ne,
rcases h with ⟨a⟩,
exfalso,
exact ne (mem_range.2 ⟨a, rfl⟩) },
{ assume empty,
have : (@const α ennreal _ c) ⁻¹' {c} ∩ s = ∅,
{ ext a, exfalso, exact h ⟨a⟩ },
simp only [this, volume_empty, mul_zero] } }
end
... = c * volume s : by rw [this, univ_inter]
lemma integral_sup_le (f g : α →ₛ ennreal) : f.integral ⊔ g.integral ≤ (f ⊔ g).integral :=
calc f.integral ⊔ g.integral =
((pair f g).map prod.fst).integral ⊔ ((pair f g).map prod.snd).integral : rfl
... ≤ (pair f g).range.sum (λx, (x.1 ⊔ x.2) * volume (pair f g ⁻¹' {x})) :
begin
rw [map_integral, map_integral],
refine sup_le _ _;
refine finset.sum_le_sum (λ a _, canonically_ordered_semiring.mul_le_mul _ (le_refl _)),
exact le_sup_left,
exact le_sup_right
end
... = (f ⊔ g).integral : by rw [sup_eq_map₂, map_integral]
lemma integral_le_integral (f g : α →ₛ ennreal) (h : f ≤ g) : f.integral ≤ g.integral :=
calc f.integral ≤ f.integral ⊔ g.integral : le_sup_left
... ≤ (f ⊔ g).integral : integral_sup_le _ _
... = g.integral : by rw [sup_of_le_right h]
lemma integral_congr (f g : α →ₛ ennreal) (h : ∀ₘ a, f a = g a) :
f.integral = g.integral :=
show ((pair f g).map prod.fst).integral = ((pair f g).map prod.snd).integral, from
begin
rw [map_integral, map_integral],
refine finset.sum_congr rfl (assume p hp, _),
rcases mem_range.1 hp with ⟨a, rfl⟩,
by_cases eq : f a = g a,
{ dsimp only [pair_apply], rw eq },
{ have : volume ((pair f g) ⁻¹' {(f a, g a)}) = 0,
{ refine volume_mono_null (assume a' ha', _) h,
simp at ha',
show f a' ≠ g a',
rwa [ha'.1, ha'.2] },
simp [this] }
end
lemma integral_map {β} [measure_space β] (f : α →ₛ ennreal) (g : β →ₛ ennreal)(m : α → β)
(eq : ∀a:α, f a = g (m a)) (h : ∀s:set β, is_measurable s → volume s = volume (m ⁻¹' s)) :
f.integral = g.integral :=
have f_eq : (f : α → ennreal) = g ∘ m := funext eq,
have vol_f : ∀r, volume (f ⁻¹' {r}) = volume (g ⁻¹' {r}),
by { assume r, rw [h, f_eq, preimage_comp], exact measurable_sn _ _ },
begin
simp [integral, vol_f],
refine finset.sum_subset _ _,
{ simp [finset.subset_iff, f_eq],
rintros r a rfl, exact ⟨_, rfl⟩ },
{ assume r hrg hrf,
rw [simple_func.mem_range, not_exists] at hrf,
have : f ⁻¹' {r} = ∅ := set.eq_empty_of_subset_empty (assume a, by simpa using hrf a),
simp [(vol_f _).symm, this] }
end
end measure
section fin_vol_supp
variables [measure_space α] [has_zero β] [has_zero γ]
open finset ennreal
protected def fin_vol_supp (f : α →ₛ β) : Prop := ∀b ≠ 0, volume (f ⁻¹' {b}) < ⊤
lemma fin_vol_supp_map {f : α →ₛ β} {g : β → γ} (hf : f.fin_vol_supp) (hg : g 0 = 0) :
(f.map g).fin_vol_supp :=
begin
assume c hc,
simp only [map_preimage, volume_bUnion_preimage],
apply sum_lt_top,
intro b,
simp only [mem_filter, mem_range, mem_singleton_iff, and_imp, exists_imp_distrib],
intros a fab gbc,
apply hf,
intro b0,
rw [b0, hg] at gbc, rw gbc at hc,
contradiction
end
lemma fin_vol_supp_of_fin_vol_supp_map (f : α →ₛ β) {g : β → γ} (h : (f.map g).fin_vol_supp)
(hg : ∀b, g b = 0 → b = 0) : f.fin_vol_supp :=
begin
assume b hb,
by_cases b_mem : b ∈ f.range,
{ have gb0 : g b ≠ 0, { assume h, have := hg b h, contradiction },
have : f ⁻¹' {b} ⊆ (f.map g) ⁻¹' {g b},
rw [coe_map, @preimage_comp _ _ _ f g, preimage_subset_preimage_iff],
{ simp only [set.mem_preimage, set.mem_singleton, set.singleton_subset_iff] },
{ rw singleton_subset_iff, rw mem_range at b_mem, exact b_mem },
exact lt_of_le_of_lt (volume_mono this) (h (g b) gb0) },
{ rw ← preimage_eq_empty_iff at b_mem,
rw [b_mem, volume_empty],
exact with_top.zero_lt_top }
end
lemma fin_vol_supp_pair {f : α →ₛ β} {g : α →ₛ γ} (hf : f.fin_vol_supp) (hg : g.fin_vol_supp) :
(pair f g).fin_vol_supp :=
begin
rintros ⟨b, c⟩ hbc,
rw [pair_preimage_singleton],
rw [ne.def, prod.eq_iff_fst_eq_snd_eq, not_and_distrib] at hbc,
refine or.elim hbc (λ h : b≠0, _) (λ h : c≠0, _),
{ calc _ ≤ volume (f ⁻¹' {b}) : volume_mono (set.inter_subset_left _ _)
... < ⊤ : hf _ h },
{ calc _ ≤ volume (g ⁻¹' {c}) : volume_mono (set.inter_subset_right _ _)
... < ⊤ : hg _ h },
end
lemma integral_lt_top_of_fin_vol_supp {f : α →ₛ ennreal} (h₁ : ∀ₘ a, f a < ⊤) (h₂ : f.fin_vol_supp) :
integral f < ⊤ :=
begin
rw integral, apply sum_lt_top,
intros a ha,
have : f ⁻¹' {⊤} = -{a : α | f a < ⊤}, { ext, simp },
have vol_top : volume (f ⁻¹' {⊤}) = 0, { rw [this, volume, ← measure.mem_a_e_iff], exact h₁ },
by_cases hat : a = ⊤,
{ rw [hat, vol_top, mul_zero], exact with_top.zero_lt_top },
{ by_cases haz : a = 0,
{ rw [haz, zero_mul], exact with_top.zero_lt_top },
apply mul_lt_top,
{ rw ennreal.lt_top_iff_ne_top, exact hat },
apply h₂,
exact haz }
end
lemma fin_vol_supp_of_integral_lt_top {f : α →ₛ ennreal} (h : integral f < ⊤) : f.fin_vol_supp :=
begin
assume b hb,
rw [integral, sum_lt_top_iff] at h,
by_cases b_mem : b ∈ f.range,
{ rw ennreal.lt_top_iff_ne_top,
have h : ¬ _ = ⊤ := ennreal.lt_top_iff_ne_top.1 (h b b_mem),
simp only [mul_eq_top, not_or_distrib, not_and_distrib] at h,
rcases h with ⟨h, h'⟩,
refine or.elim h (λh, by contradiction) (λh, h) },
{ rw ← preimage_eq_empty_iff at b_mem,
rw [b_mem, volume_empty],
exact with_top.zero_lt_top }
end
/-- A technical lemma dealing with the definition of `integrable` in `l1_space.lean`. -/
lemma integral_map_coe_lt_top {f : α →ₛ β} {g : β → nnreal} (h : f.fin_vol_supp) (hg : g 0 = 0) :
integral (f.map ((coe : nnreal → ennreal) ∘ g)) < ⊤ :=
integral_lt_top_of_fin_vol_supp
(by { filter_upwards[], assume a, simp only [mem_set_of_eq, map_apply], exact ennreal.coe_lt_top})
(by { apply fin_vol_supp_map h, simp only [hg, function.comp_app, ennreal.coe_zero] })
end fin_vol_supp
end simple_func
section lintegral
open simple_func
variable [measure_space α]
/-- The lower Lebesgue integral -/
def lintegral (f : α → ennreal) : ennreal :=
⨆ (s : α →ₛ ennreal) (hf : f ≥ s), s.integral
notation `∫⁻` binders `, ` r:(scoped f, lintegral f) := r
theorem simple_func.lintegral_eq_integral (f : α →ₛ ennreal) : (∫⁻ a, f a) = f.integral :=
le_antisymm
(supr_le $ assume s, supr_le $ assume hs, integral_le_integral _ _ hs)
(le_supr_of_le f $ le_supr_of_le (le_refl f) $ le_refl _)
lemma lintegral_le_lintegral (f g : α → ennreal) (h : f ≤ g) : (∫⁻ a, f a) ≤ (∫⁻ a, g a) :=
supr_le_supr $ assume s, supr_le $ assume hs, le_supr_of_le (le_trans hs h) (le_refl _)
lemma lintegral_eq_nnreal (f : α → ennreal) :
(∫⁻ a, f a) =
(⨆ (s : α →ₛ nnreal) (hf : f ≥ s.map (coe : nnreal → ennreal)), (s.map (coe : nnreal → ennreal)).integral) :=
begin
let c : nnreal → ennreal := coe,
refine le_antisymm
(supr_le $ assume s, supr_le $ assume hs, _)
(supr_le $ assume s, supr_le $ assume hs, le_supr_of_le (s.map c) $ le_supr _ hs),
by_cases ∀ₘ a, s a ≠ ⊤,
{ have : f ≥ (s.map ennreal.to_nnreal).map c :=
le_trans (assume a, ennreal.coe_to_nnreal_le_self) hs,
refine le_supr_of_le (s.map ennreal.to_nnreal) (le_supr_of_le this (le_of_eq $ integral_congr _ _ _)),
exact filter.mem_sets_of_superset h (assume a ha, (ennreal.coe_to_nnreal ha).symm) },
{ have h_vol_s : volume {a : α | s a = ⊤} ≠ 0,
{ simp [measure_theory.all_ae_iff, set.compl_set_of] at h, assumption },
let n : ℕ → (α →ₛ nnreal) := λn, restrict (const α (n : nnreal)) (s ⁻¹' {⊤}),
have n_le_s : ∀i, (n i).map c ≤ s,
{ assume i a,
dsimp [n, c],
rw [restrict_apply _ (s.preimage_measurable _)],
split_ifs with ha,
{ simp at ha, exact ha.symm ▸ le_top },
{ exact zero_le _ } },
have approx_s : ∀ (i : ℕ), ↑i * volume {a : α | s a = ⊤} ≤ integral (map c (n i)),
{ assume i,
have : {a : α | s a = ⊤} = s ⁻¹' {⊤}, { ext a, simp },
rw [this, ← restrict_const_integral _ _ (s.preimage_measurable _)],
{ refine integral_le_integral _ _ (assume a, le_of_eq _),
simp [n, c, restrict_apply, s.preimage_measurable],
split_ifs; simp [ennreal.coe_nat] },
},
calc s.integral ≤ ⊤ : le_top
... = (⨆i:ℕ, (i : ennreal) * volume {a | s a = ⊤}) :
by rw [← ennreal.supr_mul, ennreal.supr_coe_nat, ennreal.top_mul, if_neg h_vol_s]
... ≤ (⨆i, ((n i).map c).integral) : supr_le_supr approx_s
... ≤ ⨆ (s : α →ₛ nnreal) (hf : f ≥ s.map c), (s.map c).integral :
have ∀i, ((n i).map c : α → ennreal) ≤ f := assume i, le_trans (n_le_s i) hs,
(supr_le $ assume i, le_supr_of_le (n i) (le_supr (λh, ((n i).map c).integral) (this i))) }
end
/-- Monotone convergence theorem -- somtimes called Beppo-Levi convergence.
See `lintegral_supr_directed` for a more general form. -/
theorem lintegral_supr
{f : ℕ → α → ennreal} (hf : ∀n, measurable (f n)) (h_mono : monotone f) :
(∫⁻ a, ⨆n, f n a) = (⨆n, ∫⁻ a, f n a) :=
let c : nnreal → ennreal := coe in
let F (a:α) := ⨆n, f n a in
have hF : measurable F := measurable.supr hf,
show (∫⁻ a, F a) = (⨆n, ∫⁻ a, f n a),
begin
refine le_antisymm _ _,
{ rw [lintegral_eq_nnreal],
refine supr_le (assume s, supr_le (assume hsf, _)),
refine ennreal.le_of_forall_lt_one_mul_lt (assume a ha, _),
rcases ennreal.lt_iff_exists_coe.1 ha with ⟨r, rfl, ha⟩,
have ha : r < 1 := ennreal.coe_lt_coe.1 ha,
let rs := s.map (λa, r * a),
have eq_rs : (const α r : α →ₛ ennreal) * map c s = rs.map c,
{ ext1 a, exact ennreal.coe_mul.symm },
have eq : ∀p, (rs.map c) ⁻¹' {p} = (⋃n, (rs.map c) ⁻¹' {p} ∩ {a | p ≤ f n a}),
{ assume p,
rw [← inter_Union, ← inter_univ ((map c rs) ⁻¹' {p})] {occs := occurrences.pos [1]},
refine set.ext (assume x, and_congr_right $ assume hx, (true_iff _).2 _),
by_cases p_eq : p = 0, { simp [p_eq] },
simp at hx, subst hx,
have : r * s x ≠ 0, { rwa [(≠), ← ennreal.coe_eq_zero] },
have : s x ≠ 0, { refine mt _ this, assume h, rw [h, mul_zero] },
have : (rs.map c) x < ⨆ (n : ℕ), f n x,
{ refine lt_of_lt_of_le (ennreal.coe_lt_coe.2 (_)) (hsf x),
suffices : r * s x < 1 * s x, simpa [rs],
exact mul_lt_mul_of_pos_right ha (zero_lt_iff_ne_zero.2 this) },
rcases lt_supr_iff.1 this with ⟨i, hi⟩,
exact mem_Union.2 ⟨i, le_of_lt hi⟩ },
have mono : ∀r:ennreal, monotone (λn, (rs.map c) ⁻¹' {r} ∩ {a | r ≤ f n a}),
{ assume r i j h,
refine inter_subset_inter (subset.refl _) _,
assume x hx, exact le_trans hx (h_mono h x) },
have h_meas : ∀n, is_measurable {a : α | ⇑(map c rs) a ≤ f n a} :=
assume n, is_measurable_le (simple_func.measurable _) (hf n),
calc (r:ennreal) * integral (s.map c) = (rs.map c).range.sum (λr, r * volume ((rs.map c) ⁻¹' {r})) :
by rw [← const_mul_integral, integral, eq_rs]
... ≤ (rs.map c).range.sum (λr, r * volume (⋃n, (rs.map c) ⁻¹' {r} ∩ {a | r ≤ f n a})) :
le_of_eq (finset.sum_congr rfl $ assume x hx, by rw ← eq)
... ≤ (rs.map c).range.sum (λr, (⨆n, r * volume ((rs.map c) ⁻¹' {r} ∩ {a | r ≤ f n a}))) :
le_of_eq (finset.sum_congr rfl $ assume x hx,
begin
rw [volume, measure_Union_eq_supr_nat _ (mono x), ennreal.mul_supr],
{ assume i,
refine is_measurable.inter ((rs.map c).preimage_measurable _) _,
refine (hf i).preimage _,
exact is_measurable_of_is_closed (is_closed_ge' _) }
end)
... ≤ ⨆n, (rs.map c).range.sum (λr, r * volume ((rs.map c) ⁻¹' {r} ∩ {a | r ≤ f n a})) :
begin
refine le_of_eq _,
rw [ennreal.finset_sum_supr_nat],
assume p i j h,
exact canonically_ordered_semiring.mul_le_mul (le_refl _) (volume_mono $ mono p h)
end
... ≤ (⨆n:ℕ, ((rs.map c).restrict {a | (rs.map c) a ≤ f n a}).integral) :
begin
refine supr_le_supr (assume n, _),
rw [restrict_integral _ _ (h_meas n)],
{ refine le_of_eq (finset.sum_congr rfl $ assume r hr, _),
congr' 2,
ext a,
refine and_congr_right _,
simp {contextual := tt} }
end
... ≤ (⨆n, ∫⁻ a, f n a) :
begin
refine supr_le_supr (assume n, _),
rw [← simple_func.lintegral_eq_integral],
refine lintegral_le_lintegral _ _ (assume a, _),
dsimp,
rw [restrict_apply],
split_ifs; simp, simpa using h,
exact h_meas n
end },
{ exact supr_le (assume n, lintegral_le_lintegral _ _ $ assume a, le_supr _ n) }
end
lemma lintegral_eq_supr_eapprox_integral {f : α → ennreal} (hf : measurable f) :
(∫⁻ a, f a) = (⨆n, (eapprox f n).integral) :=
calc (∫⁻ a, f a) = (∫⁻ a, ⨆n, (eapprox f n : α → ennreal) a) :
by congr; ext a; rw [supr_eapprox_apply f hf]
... = (⨆n, ∫⁻ a, (eapprox f n : α → ennreal) a) :
begin
rw [lintegral_supr],
{ assume n, exact (eapprox f n).measurable },
{ assume i j h, exact (monotone_eapprox f h) }
end
... = (⨆n, (eapprox f n).integral) : by congr; ext n; rw [(eapprox f n).lintegral_eq_integral]
lemma lintegral_add {f g : α → ennreal} (hf : measurable f) (hg : measurable g) :
(∫⁻ a, f a + g a) = (∫⁻ a, f a) + (∫⁻ a, g a) :=
calc (∫⁻ a, f a + g a) =
(∫⁻ a, (⨆n, (eapprox f n : α → ennreal) a) + (⨆n, (eapprox g n : α → ennreal) a)) :
by congr; funext a; rw [supr_eapprox_apply f hf, supr_eapprox_apply g hg]
... = (∫⁻ a, (⨆n, (eapprox f n + eapprox g n : α → ennreal) a)) :
begin
congr, funext a,
rw [ennreal.supr_add_supr_of_monotone], { refl },
{ assume i j h, exact monotone_eapprox _ h a },
{ assume i j h, exact monotone_eapprox _ h a },
end
... = (⨆n, (eapprox f n).integral + (eapprox g n).integral) :
begin
rw [lintegral_supr],
{ congr, funext n, rw [← simple_func.add_integral, ← simple_func.lintegral_eq_integral], refl },
{ assume n, exact measurable.add (eapprox f n).measurable (eapprox g n).measurable },
{ assume i j h a, exact add_le_add' (monotone_eapprox _ h _) (monotone_eapprox _ h _) }
end
... = (⨆n, (eapprox f n).integral) + (⨆n, (eapprox g n).integral) :
by refine (ennreal.supr_add_supr_of_monotone _ _).symm;
{ assume i j h, exact simple_func.integral_le_integral _ _ (monotone_eapprox _ h) }
... = (∫⁻ a, f a) + (∫⁻ a, g a) :
by rw [lintegral_eq_supr_eapprox_integral hf, lintegral_eq_supr_eapprox_integral hg]
@[simp] lemma lintegral_zero : (∫⁻ a:α, 0) = 0 :=
show (∫⁻ a:α, (0 : α →ₛ ennreal) a) = 0, by rw [simple_func.lintegral_eq_integral, zero_integral]
lemma lintegral_finset_sum (s : finset β) {f : β → α → ennreal} (hf : ∀b, measurable (f b)) :
(∫⁻ a, s.sum (λb, f b a)) = s.sum (λb, ∫⁻ a, f b a) :=
begin
refine finset.induction_on s _ _,
{ simp },
{ assume a s has ih,
simp [has],
rw [lintegral_add (hf _) (measurable_finset_sum s hf), ih] }
end
lemma lintegral_const_mul (r : ennreal) {f : α → ennreal} (hf : measurable f) :
(∫⁻ a, r * f a) = r * (∫⁻ a, f a) :=
calc (∫⁻ a, r * f a) = (∫⁻ a, (⨆n, (const α r * eapprox f n) a)) :
by congr; funext a; rw [← supr_eapprox_apply f hf, ennreal.mul_supr]; refl
... = (⨆n, r * (eapprox f n).integral) :
begin
rw [lintegral_supr],
{ congr, funext n, rw [← simple_func.const_mul_integral, ← simple_func.lintegral_eq_integral] },
{ assume n, exact simple_func.measurable _ },
{ assume i j h a, exact canonically_ordered_semiring.mul_le_mul (le_refl _)
(monotone_eapprox _ h _) }
end
... = r * (∫⁻ a, f a) : by rw [← ennreal.mul_supr, lintegral_eq_supr_eapprox_integral hf]
lemma lintegral_const_mul_le (r : ennreal) (f : α → ennreal) : r * (∫⁻ a, f a) ≤ (∫⁻ a, r * f a) :=
begin
rw [lintegral, ennreal.mul_supr],
refine supr_le (λs, _),
rw [ennreal.mul_supr],
simp only [supr_le_iff, ge_iff_le],
assume hs,
rw ← simple_func.const_mul_integral,
refine le_supr_of_le (const α r * s) (le_supr_of_le (λx, _) (le_refl _)),
exact canonically_ordered_semiring.mul_le_mul (le_refl _) (hs x)
end
lemma lintegral_const_mul' (r : ennreal) (f : α → ennreal) (hr : r ≠ ⊤) :
(∫⁻ a, r * f a) = r * (∫⁻ a, f a) :=
begin
by_cases h : r = 0,
{ simp [h] },
apply le_antisymm _ (lintegral_const_mul_le r f),
have rinv : r * r⁻¹ = 1 := ennreal.mul_inv_cancel h hr,
have rinv' : r ⁻¹ * r = 1, by { rw mul_comm, exact rinv },
have := lintegral_const_mul_le (r⁻¹) (λx, r * f x),
simp [(mul_assoc _ _ _).symm, rinv'] at this,
simpa [(mul_assoc _ _ _).symm, rinv]
using canonically_ordered_semiring.mul_le_mul (le_refl r) this
end
lemma lintegral_supr_const (r : ennreal) {s : set α} (hs : is_measurable s) :
(∫⁻ a, ⨆(h : a ∈ s), r) = r * volume s :=
begin
rw [← restrict_const_integral r s hs, ← (restrict (const α r) s).lintegral_eq_integral],
congr; ext a; by_cases a ∈ s; simp [h, hs]
end
lemma lintegral_le_lintegral_ae {f g : α → ennreal} (h : ∀ₘ a, f a ≤ g a) :
(∫⁻ a, f a) ≤ (∫⁻ a, g a) :=
begin
rcases exists_is_measurable_superset_of_measure_eq_zero h with ⟨t, hts, ht, ht0⟩,
have : - t ∈ (@measure_space.μ α _).a_e,
{ rw [measure.mem_a_e_iff, lattice.neg_neg, ht0] },
refine (supr_le $ assume s, supr_le $ assume hfs,
le_supr_of_le (s.restrict (- t)) $ le_supr_of_le _ _),
{ assume a,
by_cases a ∈ t;
simp [h, simple_func.restrict_apply, ht.compl],
exact le_trans (hfs a) (by_contradiction $ assume hnfg, h (hts hnfg)) },
{ refine le_of_eq (s.integral_congr _ _),
filter_upwards [this],
refine assume a hnt, _,
by_cases hat : a ∈ t; simp [hat, ht.compl],
exact (hnt hat).elim }
end
lemma lintegral_congr_ae {f g : α → ennreal} (h : ∀ₘ a, f a = g a) :
(∫⁻ a, f a) = (∫⁻ a, g a) :=
le_antisymm
(lintegral_le_lintegral_ae $ by filter_upwards [h] assume a h, le_of_eq h)
(lintegral_le_lintegral_ae $ by filter_upwards [h] assume a h, le_of_eq h.symm)
-- TODO: Need a better way of rewriting inside of a integral
lemma lintegral_rw₁ {f f' : α → β} (h : ∀ₘ a, f a = f' a) (g : β → ennreal) :
(∫⁻ a, g (f a)) = (∫⁻ a, g (f' a)) :=
begin
apply lintegral_congr_ae,
filter_upwards [h],
assume a,
simp only [mem_set_of_eq],
assume h,
rw h
end
-- TODO: Need a better way of rewriting inside of a integral
lemma lintegral_rw₂ {f₁ f₁' : α → β} {f₂ f₂' : α → γ} (h₁ : ∀ₘ a, f₁ a = f₁' a)
(h₂ : ∀ₘ a, f₂ a = f₂' a) (g : β → γ → ennreal) :
(∫⁻ a, g (f₁ a) (f₂ a)) = (∫⁻ a, g (f₁' a) (f₂' a)) :=
begin
apply lintegral_congr_ae,
filter_upwards [h₁, h₂],
assume a,
simp only [mem_set_of_eq],
repeat { assume h, rw h }
end
lemma simple_func.lintegral_map (f : α →ₛ β) (g : β → ennreal) :
(∫⁻ a, (f.map g) a) = ∫⁻ a, g (f a) :=
by { apply lintegral_congr_ae, filter_upwards [], assume a, exact map_apply _ _ _ }
lemma lintegral_eq_zero_iff {f : α → ennreal} (hf : measurable f) :
lintegral f = 0 ↔ (∀ₘ a, f a = 0) :=
begin
refine iff.intro (assume h, _) (assume h, _),
{ have : ∀n:ℕ, ∀ₘ a, f a < n⁻¹,
{ assume n,
have : is_measurable {a : α | f a ≥ n⁻¹ },
{ exact hf _ (is_measurable_of_is_closed $ is_closed_ge' _) },
have : (n : ennreal)⁻¹ * volume {a | f a ≥ n⁻¹ } = 0,
{ rw [← simple_func.restrict_const_integral _ _ this, ← le_zero_iff_eq,
← simple_func.lintegral_eq_integral],
refine le_trans (lintegral_le_lintegral _ _ _) (le_of_eq h),
assume a, by_cases h : (n : ennreal)⁻¹ ≤ f a; simp [h, (≥), this] },
rw [ennreal.mul_eq_zero, ennreal.inv_eq_zero] at this,
simpa [ennreal.nat_ne_top, all_ae_iff] using this },
filter_upwards [all_ae_all_iff.2 this],
dsimp,
assume a ha,
by_contradiction h,
rcases ennreal.exists_inv_nat_lt h with ⟨n, hn⟩,
exact (lt_irrefl _ $ lt_trans hn $ ha n).elim },
{ calc lintegral f = lintegral (λa:α, 0) : lintegral_congr_ae h
... = 0 : lintegral_zero }
end
/-- Weaker version of the monotone convergence theorem-/
lemma lintegral_supr_ae {f : ℕ → α → ennreal} (hf : ∀n, measurable (f n))
(h_mono : ∀n, ∀ₘ a, f n a ≤ f n.succ a) :
(∫⁻ a, ⨆n, f n a) = (⨆n, ∫⁻ a, f n a) :=
let ⟨s, hs⟩ := exists_is_measurable_superset_of_measure_eq_zero
(all_ae_iff.1 (all_ae_all_iff.2 h_mono)) in
let g := λ n a, if a ∈ s then 0 else f n a in
have g_eq_f : ∀ₘ a, ∀n, g n a = f n a,
begin
have := hs.2.2, rw [← compl_compl s] at this,
filter_upwards [(measure.mem_a_e_iff (-s)).2 this] assume a ha n, if_neg ha
end,
calc
(∫⁻ a, ⨆n, f n a) = (∫⁻ a, ⨆n, g n a) :
lintegral_congr_ae
begin
filter_upwards [g_eq_f], assume a ha, congr, funext, exact (ha n).symm
end
... = ⨆n, (∫⁻ a, g n a) :
lintegral_supr
(assume n, measurable.if hs.2.1 measurable_const (hf n))
(monotone_of_monotone_nat $ assume n a, classical.by_cases
(assume h : a ∈ s, by simp [g, if_pos h])
(assume h : a ∉ s,
begin
simp only [g, if_neg h], have := hs.1, rw subset_def at this, have := mt (this a) h,
simp only [not_not, mem_set_of_eq] at this, exact this n
end))
... = ⨆n, (∫⁻ a, f n a) :
begin
congr, funext, apply lintegral_congr_ae, filter_upwards [g_eq_f] assume a ha, ha n
end
lemma lintegral_sub {f g : α → ennreal} (hf : measurable f) (hg : measurable g)
(hg_fin : lintegral g < ⊤) (h_le : ∀ₘ a, g a ≤ f a) :
(∫⁻ a, f a - g a) = (∫⁻ a, f a) - (∫⁻ a, g a) :=
begin
rw [← ennreal.add_right_inj hg_fin,
ennreal.sub_add_cancel_of_le (lintegral_le_lintegral_ae h_le),
← lintegral_add (ennreal.measurable.sub hf hg) hg],
show (∫⁻ (a : α), f a - g a + g a) = ∫⁻ (a : α), f a,
apply lintegral_congr_ae, filter_upwards [h_le], simp only [add_comm, mem_set_of_eq],
assume a ha, exact ennreal.add_sub_cancel_of_le ha
end
/-- Monotone convergence theorem for nonincreasing sequences of functions -/
lemma lintegral_infi_ae
{f : ℕ → α → ennreal} (h_meas : ∀n, measurable (f n))
(h_mono : ∀n:ℕ, ∀ₘ a, f n.succ a ≤ f n a) (h_fin : lintegral (f 0) < ⊤) :
(∫⁻ a, ⨅n, f n a) = (⨅n, ∫⁻ a, f n a) :=
have fn_le_f0 : (∫⁻ a, ⨅n, f n a) ≤ lintegral (f 0), from
lintegral_le_lintegral _ _ (assume a, infi_le_of_le 0 (le_refl _)),
have fn_le_f0' : (⨅n, ∫⁻ a, f n a) ≤ lintegral (f 0), from infi_le_of_le 0 (le_refl _),
(ennreal.sub_left_inj h_fin fn_le_f0 fn_le_f0').1 $
show lintegral (f 0) - (∫⁻ a, ⨅n, f n a) = lintegral (f 0) - (⨅n, ∫⁻ a, f n a), from
calc
lintegral (f 0) - (∫⁻ a, ⨅n, f n a) = ∫⁻ a, f 0 a - ⨅n, f n a :
(lintegral_sub (h_meas 0) (measurable.infi h_meas)
(calc
(∫⁻ a, ⨅n, f n a) ≤ lintegral (f 0) : lintegral_le_lintegral _ _
(assume a, infi_le _ _)
... < ⊤ : h_fin )
(all_ae_of_all $ assume a, infi_le _ _)).symm
... = ∫⁻ a, ⨆n, f 0 a - f n a : congr rfl (funext (assume a, ennreal.sub_infi))
... = ⨆n, ∫⁻ a, f 0 a - f n a :
lintegral_supr_ae
(assume n, ennreal.measurable.sub (h_meas 0) (h_meas n))
(assume n, by
filter_upwards [h_mono n] assume a ha, ennreal.sub_le_sub (le_refl _) ha)
... = ⨆n, lintegral (f 0) - ∫⁻ a, f n a :
have h_mono : ∀ₘ a, ∀n:ℕ, f n.succ a ≤ f n a := all_ae_all_iff.2 h_mono,
have h_mono : ∀n, ∀ₘa, f n a ≤ f 0 a := assume n,
begin
filter_upwards [h_mono], simp only [mem_set_of_eq], assume a, assume h, induction n with n ih,
{exact le_refl _}, {exact le_trans (h n) ih}
end,
congr rfl (funext $ assume n, lintegral_sub (h_meas _) (h_meas _)
(calc
(∫⁻ a, f n a) ≤ ∫⁻ a, f 0 a : lintegral_le_lintegral_ae $ h_mono n
... < ⊤ : h_fin)
(h_mono n))
... = lintegral (f 0) - (⨅n, ∫⁻ a, f n a) : ennreal.sub_infi.symm
section priority
-- for some reason the next proof fails without changing the priority of this instance
local attribute [instance, priority 1000] classical.prop_decidable
/-- Known as Fatou's lemma -/
lemma lintegral_liminf_le {f : ℕ → α → ennreal} (h_meas : ∀n, measurable (f n)) :
(∫⁻ a, liminf at_top (λ n, f n a)) ≤ liminf at_top (λ n, lintegral (f n)) :=
calc
(∫⁻ a, liminf at_top (λ n, f n a)) = ∫⁻ a, ⨆n:ℕ, ⨅i≥n, f i a :
congr rfl (funext (assume a, liminf_eq_supr_infi_of_nat))
... = ⨆n:ℕ, ∫⁻ a, ⨅i≥n, f i a :
lintegral_supr
begin
assume n, apply measurable.infi, assume i, by_cases h : i ≥ n,
{convert h_meas i, simp [h]},
{convert measurable_const, simp [h]}
end
begin
assume n m hnm a, simp only [le_infi_iff], assume i hi,
refine infi_le_of_le i (infi_le_of_le (le_trans hnm hi) (le_refl _))
end
... ≤ ⨆n:ℕ, ⨅i≥n, lintegral (f i) :
supr_le_supr $ assume n, le_infi $
assume i, le_infi $ assume hi, lintegral_le_lintegral _ _
$ assume a, infi_le_of_le i $ infi_le_of_le hi $ le_refl _
... = liminf at_top (λ n, lintegral (f n)) : liminf_eq_supr_infi_of_nat.symm
end priority
lemma limsup_lintegral_le {f : ℕ → α → ennreal} {g : α → ennreal}
(hf_meas : ∀ n, measurable (f n)) (h_bound : ∀n, ∀ₘa, f n a ≤ g a) (h_fin : lintegral g < ⊤) :
limsup at_top (λn, lintegral (f n)) ≤ ∫⁻ a, limsup at_top (λn, f n a) :=
calc
limsup at_top (λn, lintegral (f n)) = ⨅n:ℕ, ⨆i≥n, lintegral (f i) :
limsup_eq_infi_supr_of_nat
... ≤ ⨅n:ℕ, ∫⁻ a, ⨆i≥n, f i a :
infi_le_infi $ assume n, supr_le $ assume i, supr_le $ assume hi,
lintegral_le_lintegral _ _ $ assume a, le_supr_of_le i $ le_supr_of_le hi (le_refl _)
... = ∫⁻ a, ⨅n:ℕ, ⨆i≥n, f i a :
(lintegral_infi_ae
(assume n,
@measurable.supr _ _ _ _ _ _ _ _ _ (λ i a, supr (λ (h : i ≥ n), f i a))
(assume i, measurable.supr_Prop (hf_meas i)))
(assume n, all_ae_of_all $ assume a,
begin
simp only [supr_le_iff], assume i hi, refine le_supr_of_le i _,
rw [supr_pos _], exact le_refl _, exact nat.le_of_succ_le hi
end )
(lt_of_le_of_lt
(lintegral_le_lintegral_ae
begin
filter_upwards [all_ae_all_iff.2 h_bound],
simp only [supr_le_iff, mem_set_of_eq],
assume a ha i hi, exact ha i
end )
h_fin)).symm
... = ∫⁻ a, limsup at_top (λn, f n a) :
lintegral_congr_ae $ all_ae_of_all $ assume a, limsup_eq_infi_supr_of_nat.symm
/-- Dominated convergence theorem for nonnegative functions -/
lemma tendsto_lintegral_of_dominated_convergence
{F : ℕ → α → ennreal} {f : α → ennreal} (bound : α → ennreal)
(hF_meas : ∀n, measurable (F n)) (h_bound : ∀n, ∀ₘ a, F n a ≤ bound a)
(h_fin : lintegral bound < ⊤)
(h_lim : ∀ₘ a, tendsto (λ n, F n a) at_top (𝓝 (f a))) :
tendsto (λn, lintegral (F n)) at_top (𝓝 (lintegral f)) :=
begin
have limsup_le_lintegral :=
calc
limsup at_top (λ (n : ℕ), lintegral (F n)) ≤ ∫⁻ (a : α), limsup at_top (λn, F n a) :
limsup_lintegral_le hF_meas h_bound h_fin
... = lintegral f :
lintegral_congr_ae $
by filter_upwards [h_lim] assume a h, limsup_eq_of_tendsto at_top_ne_bot h,
have lintegral_le_liminf :=
calc
lintegral f = ∫⁻ (a : α), liminf at_top (λ (n : ℕ), F n a) :
lintegral_congr_ae $
by filter_upwards [h_lim] assume a h, (liminf_eq_of_tendsto at_top_ne_bot h).symm
... ≤ liminf at_top (λ n, lintegral (F n)) :
lintegral_liminf_le hF_meas,
have liminf_eq_limsup :=
le_antisymm
(liminf_le_limsup (map_ne_bot at_top_ne_bot))
(le_trans limsup_le_lintegral lintegral_le_liminf),
have liminf_eq_lintegral : liminf at_top (λ n, lintegral (F n)) = lintegral f :=
le_antisymm (by convert limsup_le_lintegral) lintegral_le_liminf,
have limsup_eq_lintegral : limsup at_top (λ n, lintegral (F n)) = lintegral f :=
le_antisymm
limsup_le_lintegral
begin convert lintegral_le_liminf, exact liminf_eq_limsup.symm end,
exact tendsto_of_liminf_eq_limsup ⟨liminf_eq_lintegral, limsup_eq_lintegral⟩
end
/-- Dominated convergence theorem for filters with a countable basis -/
lemma tendsto_lintegral_filter_of_dominated_convergence {ι} {l : filter ι}
{F : ι → α → ennreal} {f : α → ennreal} (bound : α → ennreal)
(hl_cb : l.has_countable_basis)
(hF_meas : ∀ᶠ n in l, measurable (F n))
(h_bound : ∀ᶠ n in l, ∀ₘ a, F n a ≤ bound a)
(h_fin : lintegral bound < ⊤)
(h_lim : ∀ₘ a, tendsto (λ n, F n a) l (nhds (f a))) :
tendsto (λn, lintegral (F n)) l (nhds (lintegral f)) :=
begin
rw hl_cb.tendsto_iff_seq_tendsto,
{ intros x xl,
have hxl, { rw tendsto_at_top' at xl, exact xl },
have h := inter_mem_sets hF_meas h_bound,
replace h := hxl _ h,
rcases h with ⟨k, h⟩,
rw ← tendsto_add_at_top_iff_nat k,
refine tendsto_lintegral_of_dominated_convergence _ _ _ _ _,
{ exact bound },
{ intro, refine (h _ _).1, exact nat.le_add_left _ _ },
{ intro, refine (h _ _).2, exact nat.le_add_left _ _ },
{ assumption },
{ filter_upwards [h_lim],
simp only [mem_set_of_eq],
assume a h_lim,
apply @tendsto.comp _ _ _ (λn, x (n + k)) (λn, F n a),
{ assumption },
rw tendsto_add_at_top_iff_nat,
assumption } },
end
section
open encodable
/-- Monotone convergence for a suprema over a directed family and indexed by an encodable type -/
theorem lintegral_supr_directed [encodable β] {f : β → α → ennreal}
(hf : ∀b, measurable (f b)) (h_directed : directed (≤) f) :
(∫⁻ a, ⨆b, f b a) = (⨆b, ∫⁻ a, f b a) :=
begin
by_cases hβ : ¬ nonempty β,
{ have : ∀f : β → ennreal, (⨆(b : β), f b) = 0 :=
assume f, supr_eq_bot.2 (assume b, (hβ ⟨b⟩).elim),
simp [this] },
cases of_not_not hβ with b,
haveI iβ : inhabited β := ⟨b⟩, clear hβ b,
have : ∀a, (⨆ b, f b a) = (⨆ n, f (h_directed.sequence f n) a),
{ assume a,
refine le_antisymm (supr_le $ assume b, _) (supr_le $ assume n, le_supr (λn, f n a) _),
exact le_supr_of_le (encode b + 1) (h_directed.le_sequence b a) },
calc (∫⁻ a, ⨆ b, f b a) = (∫⁻ a, ⨆ n, f (h_directed.sequence f n) a) :
by simp only [this]
... = (⨆ n, ∫⁻ a, f (h_directed.sequence f n) a) :
lintegral_supr (assume n, hf _) h_directed.sequence_mono
... = (⨆ b, ∫⁻ a, f b a) :
begin
refine le_antisymm (supr_le $ assume n, _) (supr_le $ assume b, _),
{ exact le_supr (λb, lintegral (f b)) _ },
{ exact le_supr_of_le (encode b + 1)
(lintegral_le_lintegral _ _ $ h_directed.le_sequence b) }
end
end
end
lemma lintegral_tsum [encodable β] {f : β → α → ennreal} (hf : ∀i, measurable (f i)) :
(∫⁻ a, ∑ i, f i a) = (∑ i, ∫⁻ a, f i a) :=
begin
simp only [ennreal.tsum_eq_supr_sum],
rw [lintegral_supr_directed],
{ simp [lintegral_finset_sum _ hf] },
{ assume b, exact measurable_finset_sum _ hf },
{ assume s t,
use [s ∪ t],
split,
exact assume a, finset.sum_le_sum_of_subset (finset.subset_union_left _ _),
exact assume a, finset.sum_le_sum_of_subset (finset.subset_union_right _ _) }
end
end lintegral
namespace measure
def integral [measurable_space α] (m : measure α) (f : α → ennreal) : ennreal :=
@lintegral α { μ := m } f
variables [measurable_space α] {m : measure α}
@[simp] lemma integral_zero : m.integral (λa, 0) = 0 := @lintegral_zero α { μ := m }
lemma integral_map [measurable_space β] {f : β → ennreal} {g : α → β}
(hf : measurable f) (hg : measurable g) : (map g m).integral f = m.integral (f ∘ g) :=
begin
rw [integral, integral, lintegral_eq_supr_eapprox_integral, lintegral_eq_supr_eapprox_integral],
{ congr, funext n, symmetry,
apply simple_func.integral_map,
{ assume a, exact congr_fun (simple_func.eapprox_comp hf hg) a },
{ assume s hs, exact map_apply hg hs } },
exact hf.comp hg,
assumption
end
lemma integral_dirac (a : α) {f : α → ennreal} (hf : measurable f) : (dirac a).integral f = f a :=
have ∀f:α →ₛ ennreal, @simple_func.integral α {μ := dirac a} f = f a,
begin
assume f,
have : ∀r, @volume α { μ := dirac a } (⇑f ⁻¹' {r}) = ⨆ h : f a = r, 1,
{ assume r,
transitivity,
apply dirac_apply,
apply simple_func.measurable_sn,
refine supr_congr_Prop _ _; simp },
transitivity,
apply finset.sum_eq_single (f a),
{ assume b hb h, simp [this, ne.symm h], },
{ assume h, simp at h, exact (h a rfl).elim },
{ rw [this], simp }
end,
begin
rw [integral, lintegral_eq_supr_eapprox_integral],
{ simp [this, simple_func.supr_eapprox_apply f hf] },
assumption
end
def with_density (m : measure α) (f : α → ennreal) : measure α :=
if hf : measurable f then
measure.of_measurable (λs hs, m.integral (λa, ⨆(h : a ∈ s), f a))
(by simp)
begin
assume s hs hd,
have : ∀a, (⨆ (h : a ∈ ⋃i, s i), f a) = (∑i, (⨆ (h : a ∈ s i), f a)),
{ assume a,
by_cases ha : ∃j, a ∈ s j,
{ rcases ha with ⟨j, haj⟩,
have : ∀i, a ∈ s i ↔ j = i := assume i,
iff.intro
(assume hai, by_contradiction $ assume hij, hd j i hij ⟨haj, hai⟩)
(by rintros rfl; assumption),
simp [this, ennreal.tsum_supr_eq] },
{ have : ∀i, ¬ a ∈ s i, { simpa using ha },
simp [this] } },
simp only [this],
apply lintegral_tsum,
{ assume i,
simp [supr_eq_if],
exact measurable.if (hs i) hf measurable_const }
end
else 0
lemma with_density_apply {m : measure α} {f : α → ennreal} {s : set α}
(hf : measurable f) (hs : is_measurable s) :
m.with_density f s = m.integral (λa, ⨆(h : a ∈ s), f a) :=
by rw [with_density, dif_pos hf]; exact measure.of_measurable_apply s hs
end measure
end measure_theory