Uniform integrability #
This file will be used in the future to define uniform integrability. Uniform integrability is an important notion in both measure theory as well as probability theory. So far this file only contains the Egorov theorem which will be used to prove the Vitali convergence theorem which is one of the main results about uniform integrability.
Main results #
measure_theory.egorov: Egorov's theorem which shows that a sequence of almost everywhere convergent functions converges uniformly except on an arbitrarily small set.
We will in this section prove Egorov's theorem.
def
measure_theory.egorov.not_convergent_seq
{α : Type u_1}
{β : Type u_2}
[metric_space β]
(f : ℕ → α → β)
(g : α → β)
(i j : ℕ) :
set α
Given a sequence of functions f and a function g, not_convergent_seq f g i j is the
set of elements such that f k x and g x are separated by at least 1 / (i + 1) for some
k ≥ j.
This definition is useful for Egorov's theorem.
theorem
measure_theory.egorov.mem_not_convergent_seq_iff
{α : Type u_1}
{β : Type u_2}
[metric_space β]
{i j : ℕ}
{f : ℕ → α → β}
{g : α → β}
{x : α} :
theorem
measure_theory.egorov.not_convergent_seq_antitone
{α : Type u_1}
{β : Type u_2}
[metric_space β]
{i : ℕ}
{f : ℕ → α → β}
{g : α → β} :
theorem
measure_theory.egorov.measure_inter_not_convergent_seq_eq_zero
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
{s : set α}
{f : ℕ → α → β}
{g : α → β}
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → filter.tendsto (λ (n : ℕ), f n x) filter.at_top (𝓝 (g x)))
(i : ℕ) :
⇑μ (s ∩ ⋂ (j : ℕ), measure_theory.egorov.not_convergent_seq f g i j) = 0
theorem
measure_theory.egorov.not_convergent_seq_measurable_set
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
[metric_space β]
{i j : ℕ}
{f : ℕ → α → β}
{g : α → β}
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(hf : ∀ (n : ℕ), measurable (f n))
(hg : measurable g) :
theorem
measure_theory.egorov.measure_not_convergent_seq_tendsto_zero
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
{s : set α}
{f : ℕ → α → β}
{g : α → β}
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(hf : ∀ (n : ℕ), measurable (f n))
(hg : measurable g)
(hsm : measurable_set s)
(hs : ⇑μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → filter.tendsto (λ (n : ℕ), f n x) filter.at_top (𝓝 (g x)))
(i : ℕ) :
filter.tendsto (λ (j : ℕ), ⇑μ (s ∩ measure_theory.egorov.not_convergent_seq f g i j)) filter.at_top (𝓝 0)
theorem
measure_theory.egorov.exists_not_convergent_seq_lt
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
{s : set α}
{ε : ℝ}
{f : ℕ → α → β}
{g : α → β}
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(hε : 0 < ε)
(hf : ∀ (n : ℕ), measurable (f n))
(hg : measurable g)
(hsm : measurable_set s)
(hs : ⇑μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → filter.tendsto (λ (n : ℕ), f n x) filter.at_top (𝓝 (g x)))
(i : ℕ) :
∃ (j : ℕ), ⇑μ (s ∩ measure_theory.egorov.not_convergent_seq f g i j) ≤ ennreal.of_real (ε * 2⁻¹ ^ i)
noncomputable
def
measure_theory.egorov.not_convergent_seq_lt_index
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
{s : set α}
{ε : ℝ}
{f : ℕ → α → β}
{g : α → β}
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(hε : 0 < ε)
(hf : ∀ (n : ℕ), measurable (f n))
(hg : measurable g)
(hsm : measurable_set s)
(hs : ⇑μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → filter.tendsto (λ (n : ℕ), f n x) filter.at_top (𝓝 (g x)))
(i : ℕ) :
Given some ε > 0, not_convergent_seq_lt_index provides the index such that
not_convergent_seq (intersected with a set of finite measure) has measure less than
ε * 2⁻¹ ^ i.
This definition is useful for Egorov's theorem.
Equations
- measure_theory.egorov.not_convergent_seq_lt_index hε hf hg hsm hs hfg i = classical.some _
theorem
measure_theory.egorov.not_convergent_seq_lt_index_spec
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
{s : set α}
{ε : ℝ}
{f : ℕ → α → β}
{g : α → β}
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(hε : 0 < ε)
(hf : ∀ (n : ℕ), measurable (f n))
(hg : measurable g)
(hsm : measurable_set s)
(hs : ⇑μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → filter.tendsto (λ (n : ℕ), f n x) filter.at_top (𝓝 (g x)))
(i : ℕ) :
⇑μ (s ∩ measure_theory.egorov.not_convergent_seq f g i (measure_theory.egorov.not_convergent_seq_lt_index hε hf hg hsm hs hfg i)) ≤ ennreal.of_real (ε * 2⁻¹ ^ i)
def
measure_theory.egorov.Union_not_convergent_seq
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
{s : set α}
{ε : ℝ}
{f : ℕ → α → β}
{g : α → β}
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(hε : 0 < ε)
(hf : ∀ (n : ℕ), measurable (f n))
(hg : measurable g)
(hsm : measurable_set s)
(hs : ⇑μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → filter.tendsto (λ (n : ℕ), f n x) filter.at_top (𝓝 (g x))) :
set α
Given some ε > 0, Union_not_convergent_seq is the union of not_convergent_seq with
specific indicies such that Union_not_convergent_seq has measure less equal than ε.
This definition is useful for Egorov's theorem.
Equations
- measure_theory.egorov.Union_not_convergent_seq hε hf hg hsm hs hfg = ⋃ (i : ℕ), s ∩ measure_theory.egorov.not_convergent_seq f g i (measure_theory.egorov.not_convergent_seq_lt_index _ hf hg hsm hs hfg i)
theorem
measure_theory.egorov.Union_not_convergent_seq_measurable_set
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
{s : set α}
{ε : ℝ}
{f : ℕ → α → β}
{g : α → β}
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(hε : 0 < ε)
(hf : ∀ (n : ℕ), measurable (f n))
(hg : measurable g)
(hsm : measurable_set s)
(hs : ⇑μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → filter.tendsto (λ (n : ℕ), f n x) filter.at_top (𝓝 (g x))) :
measurable_set (measure_theory.egorov.Union_not_convergent_seq hε hf hg hsm hs hfg)
theorem
measure_theory.egorov.measure_Union_not_convergent_seq
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
{s : set α}
{ε : ℝ}
{f : ℕ → α → β}
{g : α → β}
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(hε : 0 < ε)
(hf : ∀ (n : ℕ), measurable (f n))
(hg : measurable g)
(hsm : measurable_set s)
(hs : ⇑μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → filter.tendsto (λ (n : ℕ), f n x) filter.at_top (𝓝 (g x))) :
⇑μ (measure_theory.egorov.Union_not_convergent_seq hε hf hg hsm hs hfg) ≤ ennreal.of_real ε
theorem
measure_theory.egorov.Union_not_convergent_seq_subset
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
{s : set α}
{ε : ℝ}
{f : ℕ → α → β}
{g : α → β}
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(hε : 0 < ε)
(hf : ∀ (n : ℕ), measurable (f n))
(hg : measurable g)
(hsm : measurable_set s)
(hs : ⇑μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → filter.tendsto (λ (n : ℕ), f n x) filter.at_top (𝓝 (g x))) :
measure_theory.egorov.Union_not_convergent_seq hε hf hg hsm hs hfg ⊆ s
theorem
measure_theory.egorov.tendsto_uniformly_on_diff_Union_not_convergent_seq
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
{s : set α}
{ε : ℝ}
{f : ℕ → α → β}
{g : α → β}
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(hε : 0 < ε)
(hf : ∀ (n : ℕ), measurable (f n))
(hg : measurable g)
(hsm : measurable_set s)
(hs : ⇑μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → filter.tendsto (λ (n : ℕ), f n x) filter.at_top (𝓝 (g x))) :
tendsto_uniformly_on f g filter.at_top (s \ measure_theory.egorov.Union_not_convergent_seq hε hf hg hsm hs hfg)
theorem
measure_theory.tendsto_uniformly_on_of_ae_tendsto
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
{f : ℕ → α → β}
{g : α → β}
{s : set α}
(hf : ∀ (n : ℕ), measurable (f n))
(hg : measurable g)
(hsm : measurable_set s)
(hs : ⇑μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → filter.tendsto (λ (n : ℕ), f n x) filter.at_top (𝓝 (g x)))
{ε : ℝ}
(hε : 0 < ε) :
∃ (t : set α) (H : t ⊆ s), measurable_set t ∧ ⇑μ t ≤ ennreal.of_real ε ∧ tendsto_uniformly_on f g filter.at_top (s \ t)
Egorov's theorem: If f : ℕ → α → β is a sequence of measurable functions that converges
to g : α → β almost everywhere on a measurable set s of finite measure, then for all ε > 0,
there exists a subset t ⊆ s such that μ t ≤ ε and f converges to g uniformly on s \ t.
In other words, a sequence of almost everywhere convergent functions converges uniformly except on an arbitrarily small set.
theorem
measure_theory.tendsto_uniformly_on_of_ae_tendsto'
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
{f : ℕ → α → β}
{g : α → β}
[measure_theory.is_finite_measure μ]
(hf : ∀ (n : ℕ), measurable (f n))
(hg : measurable g)
(hfg : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ℕ), f n x) filter.at_top (𝓝 (g x)))
{ε : ℝ}
(hε : 0 < ε) :
∃ (t : set α), measurable_set t ∧ ⇑μ t ≤ ennreal.of_real ε ∧ tendsto_uniformly_on f g filter.at_top tᶜ
Egorov's theorem for finite measure spaces.