# Documentation

Mathlib.MeasureTheory.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 #

• MeasureTheory.Egorov: Egorov's theorem which shows that a sequence of almost everywhere convergent functions converges uniformly except on an arbitrarily small set.
def MeasureTheory.Egorov.notConvergentSeq {α : Type u_1} {β : Type u_2} {ι : Type u_3} [] [] (f : ιαβ) (g : αβ) (n : ) (j : ι) :
Set α

Given a sequence of functions f and a function g, notConvergentSeq 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.

Instances For
theorem MeasureTheory.Egorov.mem_notConvergentSeq_iff {α : Type u_1} {β : Type u_2} {ι : Type u_3} [] {n : } {j : ι} {f : ιαβ} {g : αβ} [] {x : α} :
k x, 1 / (n + 1) < dist (f k x) (g x)
theorem MeasureTheory.Egorov.notConvergentSeq_antitone {α : Type u_1} {β : Type u_2} {ι : Type u_3} [] {n : } {f : ιαβ} {g : αβ} [] :
theorem MeasureTheory.Egorov.measure_inter_notConvergentSeq_eq_zero {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] {μ : } {s : Set α} {f : ιαβ} {g : αβ} [] [] (hfg : ∀ᵐ (x : α) ∂μ, x sFilter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) (n : ) :
μ (s ⋂ (j : ι), ) = 0
theorem MeasureTheory.Egorov.notConvergentSeq_measurableSet {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] {n : } {j : ι} {f : ιαβ} {g : αβ} [] [] (hf : ∀ (n : ι), ) (hg : ) :
theorem MeasureTheory.Egorov.measure_notConvergentSeq_tendsto_zero {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] {μ : } {s : Set α} {f : ιαβ} {g : αβ} [] [] (hf : ∀ (n : ι), ) (hg : ) (hsm : ) (hs : μ s ) (hfg : ∀ᵐ (x : α) ∂μ, x sFilter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) (n : ) :
Filter.Tendsto (fun j => μ ()) Filter.atTop (nhds 0)
theorem MeasureTheory.Egorov.exists_notConvergentSeq_lt {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] {μ : } {s : Set α} {ε : } {f : ιαβ} {g : αβ} [] [] [] (hε : 0 < ε) (hf : ∀ (n : ι), ) (hg : ) (hsm : ) (hs : μ s ) (hfg : ∀ᵐ (x : α) ∂μ, x sFilter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) (n : ) :
j, μ () ENNReal.ofReal (ε * 2⁻¹ ^ n)
def MeasureTheory.Egorov.notConvergentSeqLTIndex {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] {μ : } {s : Set α} {ε : } {f : ιαβ} {g : αβ} [] [] [] (hε : 0 < ε) (hf : ∀ (n : ι), ) (hg : ) (hsm : ) (hs : μ s ) (hfg : ∀ᵐ (x : α) ∂μ, x sFilter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) (n : ) :
ι

Given some ε > 0, notConvergentSeqLTIndex provides the index such that notConvergentSeq (intersected with a set of finite measure) has measure less than ε * 2⁻¹ ^ n.

This definition is useful for Egorov's theorem.

Instances For
theorem MeasureTheory.Egorov.notConvergentSeqLTIndex_spec {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] {μ : } {s : Set α} {ε : } {f : ιαβ} {g : αβ} [] [] [] (hε : 0 < ε) (hf : ∀ (n : ι), ) (hg : ) (hsm : ) (hs : μ s ) (hfg : ∀ᵐ (x : α) ∂μ, x sFilter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) (n : ) :
def MeasureTheory.Egorov.iUnionNotConvergentSeq {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] {μ : } {s : Set α} {ε : } {f : ιαβ} {g : αβ} [] [] [] (hε : 0 < ε) (hf : ∀ (n : ι), ) (hg : ) (hsm : ) (hs : μ s ) (hfg : ∀ᵐ (x : α) ∂μ, x sFilter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) :
Set α

Given some ε > 0, iUnionNotConvergentSeq is the union of notConvergentSeq with specific indices such that iUnionNotConvergentSeq has measure less equal than ε.

This definition is useful for Egorov's theorem.

Instances For
theorem MeasureTheory.Egorov.iUnionNotConvergentSeq_measurableSet {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] {μ : } {s : Set α} {ε : } {f : ιαβ} {g : αβ} [] [] [] (hε : 0 < ε) (hf : ∀ (n : ι), ) (hg : ) (hsm : ) (hs : μ s ) (hfg : ∀ᵐ (x : α) ∂μ, x sFilter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) :
theorem MeasureTheory.Egorov.measure_iUnionNotConvergentSeq {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] {μ : } {s : Set α} {ε : } {f : ιαβ} {g : αβ} [] [] [] (hε : 0 < ε) (hf : ∀ (n : ι), ) (hg : ) (hsm : ) (hs : μ s ) (hfg : ∀ᵐ (x : α) ∂μ, x sFilter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) :
μ (MeasureTheory.Egorov.iUnionNotConvergentSeq hf hg hsm hs hfg)
theorem MeasureTheory.Egorov.iUnionNotConvergentSeq_subset {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] {μ : } {s : Set α} {ε : } {f : ιαβ} {g : αβ} [] [] [] (hε : 0 < ε) (hf : ∀ (n : ι), ) (hg : ) (hsm : ) (hs : μ s ) (hfg : ∀ᵐ (x : α) ∂μ, x sFilter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) :
theorem MeasureTheory.Egorov.tendstoUniformlyOn_diff_iUnionNotConvergentSeq {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] {μ : } {s : Set α} {ε : } {f : ιαβ} {g : αβ} [] [] [] (hε : 0 < ε) (hf : ∀ (n : ι), ) (hg : ) (hsm : ) (hs : μ s ) (hfg : ∀ᵐ (x : α) ∂μ, x sFilter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) :
TendstoUniformlyOn f g Filter.atTop (s \ MeasureTheory.Egorov.iUnionNotConvergentSeq hf hg hsm hs hfg)
theorem MeasureTheory.tendstoUniformlyOn_of_ae_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] {μ : } [] [] [] {f : ιαβ} {g : αβ} {s : Set α} (hf : ∀ (n : ι), ) (hg : ) (hsm : ) (hs : μ s ) (hfg : ∀ᵐ (x : α) ∂μ, x sFilter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) {ε : } (hε : 0 < ε) :
t x, μ t TendstoUniformlyOn f g Filter.atTop (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 MeasureTheory.tendstoUniformlyOn_of_ae_tendsto' {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] {μ : } [] [] [] {f : ιαβ} {g : αβ} (hf : ∀ (n : ι), ) (hg : ) (hfg : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) {ε : } (hε : 0 < ε) :
t, μ t TendstoUniformlyOn f g Filter.atTop t

Egorov's theorem for finite measure spaces.