# mathlibdocumentation

measure_theory.function.egorov

# Egorov theorem #

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
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 : α} :
∃ (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 : α → β} [nonempty ι] (hfg : ∀ᵐ (x : α) ∂μ, x sfilter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (g x))) (n : ) :
μ (s ⋂ (j : ι), = 0
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 ι] [encodable ι] (hf : ∀ (n : ι), )  :
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 : α → β} [encodable ι] (hf : ∀ (n : ι), ) (hsm : measurable_set s) (hs : μ s ) (hfg : ∀ᵐ (x : α) ∂μ, x sfilter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (g x))) (n : ) :
filter.tendsto (λ (j : ι), μ (s 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 : α → β} [nonempty ι] [encodable ι] (hε : 0 < ε) (hf : ∀ (n : ι), ) (hsm : measurable_set s) (hs : μ s ) (hfg : ∀ᵐ (x : α) ∂μ, x sfilter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (g x))) (n : ) :
∃ (j : ι), μ (s 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 : α → β} [nonempty ι] [encodable ι] (hε : 0 < ε) (hf : ∀ (n : ι), ) (hsm : measurable_set s) (hs : μ s ) (hfg : ∀ᵐ (x : α) ∂μ, x sfilter.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
• hs hfg n =
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 : α → β} [nonempty ι] [encodable ι] (hε : 0 < ε) (hf : ∀ (n : ι), ) (hsm : measurable_set s) (hs : μ s ) (hfg : ∀ᵐ (x : α) ∂μ, x sfilter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (g x))) (n : ) :
μ (s 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 : α → β} [nonempty ι] [encodable ι] (hε : 0 < ε) (hf : ∀ (n : ι), ) (hsm : measurable_set s) (hs : μ s ) (hfg : ∀ᵐ (x : α) ∂μ, x sfilter.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
• hsm hs hfg = ⋃ (n : ), s 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 : α → β} [nonempty ι] [encodable ι] (hε : 0 < ε) (hf : ∀ (n : ι), ) (hsm : measurable_set s) (hs : μ s ) (hfg : ∀ᵐ (x : α) ∂μ, x sfilter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (g x))) :
measurable_set 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 : α → β} [nonempty ι] [encodable ι] (hε : 0 < ε) (hf : ∀ (n : ι), ) (hsm : measurable_set s) (hs : μ s ) (hfg : ∀ᵐ (x : α) ∂μ, x sfilter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (g x))) :
μ hsm hs hfg)
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 : α → β} [nonempty ι] [encodable ι] (hε : 0 < ε) (hf : ∀ (n : ι), ) (hsm : measurable_set s) (hs : μ s ) (hfg : ∀ᵐ (x : α) ∂μ, x sfilter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (g x))) :
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 : α → β} [nonempty ι] [encodable ι] (hε : 0 < ε) (hf : ∀ (n : ι), ) (hsm : measurable_set s) (hs : μ s ) (hfg : ∀ᵐ (x : α) ∂μ, x sfilter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (g x))) :
(s \ 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 α} [nonempty ι] [encodable ι] {f : ι → α → β} {g : α → β} {s : set α} (hf : ∀ (n : ι), ) (hsm : measurable_set s) (hs : μ s ) (hfg : ∀ᵐ (x : α) ∂μ, x sfilter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (g x))) {ε : } (hε : 0 < ε) :
∃ (t : set α) (H : t s), μ t (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 encodable, 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 α} [nonempty ι] [encodable ι] {f : ι → α → β} {g : α → β} (hf : ∀ (n : ι), ) (hfg : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ι), f n x) filter.at_top (nhds (g x))) {ε : } (hε : 0 < ε) :
∃ (t : set α), μ t

Egorov's theorem for finite measure spaces.