mathlib3 documentation

measure_theory.function.egorov

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 #

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
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 : α} :
x measure_theory.egorov.not_convergent_seq f g n j (k : ι) (hk : j k), 1 / (n + 1) < has_dist.dist (f k x) (g 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 : ) :
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 : ) :
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
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 : ) :
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
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))) :
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))) :
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))) :
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))) :
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 < ε) :

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 < ε) :

Egorov's theorem for finite measure spaces.