Egorov theorem #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file contains the Egorov theorem which states that an almost everywhere convergent sequence on a finite measure space converges uniformly except on an arbitrarily small set. This theorem is useful for the Vitali convergence theorem as well as theorems regarding convergence in measure.
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.
def
measure_theory.egorov.not_convergent_seq
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[metric_space β]
[preorder ι]
(f : ι → α → β)
(g : α → β)
(n : ℕ)
(j : ι) :
set α
Given a sequence of functions f and a function g, not_convergent_seq f g n j is the
set of elements such that f k x and g x are separated by at least 1 / (n + 1) for some
k ≥ j.
This definition is useful for Egorov's theorem.
Equations
- measure_theory.egorov.not_convergent_seq f g n j = ⋃ (k : ι) (hk : j ≤ k), {x : α | 1 / (↑n + 1) < has_dist.dist (f k x) (g x)}
theorem
measure_theory.egorov.mem_not_convergent_seq_iff
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[metric_space β]
{n : ℕ}
{j : ι}
{f : ι → α → β}
{g : α → β}
[preorder ι]
{x : α} :
theorem
measure_theory.egorov.not_convergent_seq_antitone
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[metric_space β]
{n : ℕ}
{f : ι → α → β}
{g : α → β}
[preorder ι] :
theorem
measure_theory.egorov.measure_inter_not_convergent_seq_eq_zero
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
{s : set α}
{f : ι → α → β}
{g : α → β}
[semilattice_sup ι]
[nonempty ι]
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → filter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (g x)))
(n : ℕ) :
theorem
measure_theory.egorov.not_convergent_seq_measurable_set
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space α}
[metric_space β]
{n : ℕ}
{j : ι}
{f : ι → α → β}
{g : α → β}
[preorder ι]
[countable ι]
(hf : ∀ (n : ι), measure_theory.strongly_measurable (f n))
(hg : measure_theory.strongly_measurable g) :
theorem
measure_theory.egorov.measure_not_convergent_seq_tendsto_zero
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
{s : set α}
{f : ι → α → β}
{g : α → β}
[semilattice_sup ι]
[countable ι]
(hf : ∀ (n : ι), measure_theory.strongly_measurable (f n))
(hg : measure_theory.strongly_measurable g)
(hsm : measurable_set s)
(hs : ⇑μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → filter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (g x)))
(n : ℕ) :
filter.tendsto (λ (j : ι), ⇑μ (s ∩ measure_theory.egorov.not_convergent_seq f g n j)) filter.at_top (nhds 0)
theorem
measure_theory.egorov.exists_not_convergent_seq_lt
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
{s : set α}
{ε : ℝ}
{f : ι → α → β}
{g : α → β}
[semilattice_sup ι]
[nonempty ι]
[countable ι]
(hε : 0 < ε)
(hf : ∀ (n : ι), measure_theory.strongly_measurable (f n))
(hg : measure_theory.strongly_measurable g)
(hsm : measurable_set s)
(hs : ⇑μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → filter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (g x)))
(n : ℕ) :
∃ (j : ι), ⇑μ (s ∩ measure_theory.egorov.not_convergent_seq f g n j) ≤ ennreal.of_real (ε * 2⁻¹ ^ n)
noncomputable
def
measure_theory.egorov.not_convergent_seq_lt_index
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
{s : set α}
{ε : ℝ}
{f : ι → α → β}
{g : α → β}
[semilattice_sup ι]
[nonempty ι]
[countable ι]
(hε : 0 < ε)
(hf : ∀ (n : ι), measure_theory.strongly_measurable (f n))
(hg : measure_theory.strongly_measurable g)
(hsm : measurable_set s)
(hs : ⇑μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → filter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (g x)))
(n : ℕ) :
ι
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⁻¹ ^ n.
This definition is useful for Egorov's theorem.
Equations
- measure_theory.egorov.not_convergent_seq_lt_index hε hf hg hsm hs hfg n = classical.some _
theorem
measure_theory.egorov.not_convergent_seq_lt_index_spec
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
{s : set α}
{ε : ℝ}
{f : ι → α → β}
{g : α → β}
[semilattice_sup ι]
[nonempty ι]
[countable ι]
(hε : 0 < ε)
(hf : ∀ (n : ι), measure_theory.strongly_measurable (f n))
(hg : measure_theory.strongly_measurable g)
(hsm : measurable_set s)
(hs : ⇑μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → filter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (g x)))
(n : ℕ) :
⇑μ (s ∩ measure_theory.egorov.not_convergent_seq f g n (measure_theory.egorov.not_convergent_seq_lt_index hε hf hg hsm hs hfg n)) ≤ ennreal.of_real (ε * 2⁻¹ ^ n)
def
measure_theory.egorov.Union_not_convergent_seq
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
{s : set α}
{ε : ℝ}
{f : ι → α → β}
{g : α → β}
[semilattice_sup ι]
[nonempty ι]
[countable ι]
(hε : 0 < ε)
(hf : ∀ (n : ι), measure_theory.strongly_measurable (f n))
(hg : measure_theory.strongly_measurable g)
(hsm : measurable_set s)
(hs : ⇑μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → filter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (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 = ⋃ (n : ℕ), s ∩ measure_theory.egorov.not_convergent_seq f g n (measure_theory.egorov.not_convergent_seq_lt_index _ hf hg hsm hs hfg n)
theorem
measure_theory.egorov.Union_not_convergent_seq_measurable_set
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
{s : set α}
{ε : ℝ}
{f : ι → α → β}
{g : α → β}
[semilattice_sup ι]
[nonempty ι]
[countable ι]
(hε : 0 < ε)
(hf : ∀ (n : ι), measure_theory.strongly_measurable (f n))
(hg : measure_theory.strongly_measurable g)
(hsm : measurable_set s)
(hs : ⇑μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → filter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (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}
{ι : Type u_3}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
{s : set α}
{ε : ℝ}
{f : ι → α → β}
{g : α → β}
[semilattice_sup ι]
[nonempty ι]
[countable ι]
(hε : 0 < ε)
(hf : ∀ (n : ι), measure_theory.strongly_measurable (f n))
(hg : measure_theory.strongly_measurable g)
(hsm : measurable_set s)
(hs : ⇑μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → filter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (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}
{ι : Type u_3}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
{s : set α}
{ε : ℝ}
{f : ι → α → β}
{g : α → β}
[semilattice_sup ι]
[nonempty ι]
[countable ι]
(hε : 0 < ε)
(hf : ∀ (n : ι), measure_theory.strongly_measurable (f n))
(hg : measure_theory.strongly_measurable g)
(hsm : measurable_set s)
(hs : ⇑μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → filter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (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}
{ι : Type u_3}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
{s : set α}
{ε : ℝ}
{f : ι → α → β}
{g : α → β}
[semilattice_sup ι]
[nonempty ι]
[countable ι]
(hε : 0 < ε)
(hf : ∀ (n : ι), measure_theory.strongly_measurable (f n))
(hg : measure_theory.strongly_measurable g)
(hsm : measurable_set s)
(hs : ⇑μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → filter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (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}
{ι : Type u_3}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
[semilattice_sup ι]
[nonempty ι]
[countable ι]
{f : ι → α → β}
{g : α → β}
{s : set α}
(hf : ∀ (n : ι), measure_theory.strongly_measurable (f n))
(hg : measure_theory.strongly_measurable g)
(hsm : measurable_set s)
(hs : ⇑μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → filter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (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 strongly 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. We require the index type ι to be countable, and usually ι = ℕ.
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}
{ι : Type u_3}
{m : measurable_space α}
[metric_space β]
{μ : measure_theory.measure α}
[semilattice_sup ι]
[nonempty ι]
[countable ι]
{f : ι → α → β}
{g : α → β}
[measure_theory.is_finite_measure μ]
(hf : ∀ (n : ι), measure_theory.strongly_measurable (f n))
(hg : measure_theory.strongly_measurable g)
(hfg : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (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.