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}
[MetricSpace β]
[Preorder ι]
(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.
Equations
Instances For
theorem
MeasureTheory.Egorov.mem_notConvergentSeq_iff
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[MetricSpace β]
{n : ℕ}
{j : ι}
{f : ι → α → β}
{g : α → β}
[Preorder ι]
{x : α}
:
theorem
MeasureTheory.Egorov.notConvergentSeq_antitone
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[MetricSpace β]
{n : ℕ}
{f : ι → α → β}
{g : α → β}
[Preorder ι]
:
theorem
MeasureTheory.Egorov.measure_inter_notConvergentSeq_eq_zero
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
[MetricSpace β]
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : ι → α → β}
{g : α → β}
[SemilatticeSup ι]
[Nonempty ι]
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (g x)))
(n : ℕ)
:
μ (s ∩ ⋂ (j : ι), MeasureTheory.Egorov.notConvergentSeq f g n j) = 0
theorem
MeasureTheory.Egorov.notConvergentSeq_measurableSet
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
[MetricSpace β]
{n : ℕ}
{j : ι}
{f : ι → α → β}
{g : α → β}
[Preorder ι]
[Countable ι]
(hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n))
(hg : MeasureTheory.StronglyMeasurable g)
:
theorem
MeasureTheory.Egorov.measure_notConvergentSeq_tendsto_zero
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
[MetricSpace β]
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : ι → α → β}
{g : α → β}
[SemilatticeSup ι]
[Countable ι]
(hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n))
(hg : MeasureTheory.StronglyMeasurable g)
(hsm : MeasurableSet s)
(hs : μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (g x)))
(n : ℕ)
:
Filter.Tendsto (fun (j : ι) => μ (s ∩ MeasureTheory.Egorov.notConvergentSeq f g n j)) Filter.atTop (nhds 0)
theorem
MeasureTheory.Egorov.exists_notConvergentSeq_lt
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
[MetricSpace β]
{μ : MeasureTheory.Measure α}
{s : Set α}
{ε : ℝ}
{f : ι → α → β}
{g : α → β}
[SemilatticeSup ι]
[Nonempty ι]
[Countable ι]
(hε : 0 < ε)
(hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n))
(hg : MeasureTheory.StronglyMeasurable g)
(hsm : MeasurableSet s)
(hs : μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (g x)))
(n : ℕ)
:
∃ (j : ι), μ (s ∩ MeasureTheory.Egorov.notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * 2⁻¹ ^ n)
def
MeasureTheory.Egorov.notConvergentSeqLTIndex
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
[MetricSpace β]
{μ : MeasureTheory.Measure α}
{s : Set α}
{ε : ℝ}
{f : ι → α → β}
{g : α → β}
[SemilatticeSup ι]
[Nonempty ι]
[Countable ι]
(hε : 0 < ε)
(hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n))
(hg : MeasureTheory.StronglyMeasurable g)
(hsm : MeasurableSet s)
(hs : μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.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.
Equations
- MeasureTheory.Egorov.notConvergentSeqLTIndex hε hf hg hsm hs hfg n = Classical.choose ⋯
Instances For
theorem
MeasureTheory.Egorov.notConvergentSeqLTIndex_spec
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
[MetricSpace β]
{μ : MeasureTheory.Measure α}
{s : Set α}
{ε : ℝ}
{f : ι → α → β}
{g : α → β}
[SemilatticeSup ι]
[Nonempty ι]
[Countable ι]
(hε : 0 < ε)
(hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n))
(hg : MeasureTheory.StronglyMeasurable g)
(hsm : MeasurableSet s)
(hs : μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (g x)))
(n : ℕ)
:
μ
(s ∩ MeasureTheory.Egorov.notConvergentSeq f g n
(MeasureTheory.Egorov.notConvergentSeqLTIndex hε hf hg hsm hs hfg n)) ≤ ENNReal.ofReal (ε * 2⁻¹ ^ n)
def
MeasureTheory.Egorov.iUnionNotConvergentSeq
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
[MetricSpace β]
{μ : MeasureTheory.Measure α}
{s : Set α}
{ε : ℝ}
{f : ι → α → β}
{g : α → β}
[SemilatticeSup ι]
[Nonempty ι]
[Countable ι]
(hε : 0 < ε)
(hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n))
(hg : MeasureTheory.StronglyMeasurable g)
(hsm : MeasurableSet s)
(hs : μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.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.
Equations
- MeasureTheory.Egorov.iUnionNotConvergentSeq hε hf hg hsm hs hfg = ⋃ (n : ℕ), s ∩ MeasureTheory.Egorov.notConvergentSeq f g n (MeasureTheory.Egorov.notConvergentSeqLTIndex ⋯ hf hg hsm hs hfg n)
Instances For
theorem
MeasureTheory.Egorov.iUnionNotConvergentSeq_measurableSet
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
[MetricSpace β]
{μ : MeasureTheory.Measure α}
{s : Set α}
{ε : ℝ}
{f : ι → α → β}
{g : α → β}
[SemilatticeSup ι]
[Nonempty ι]
[Countable ι]
(hε : 0 < ε)
(hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n))
(hg : MeasureTheory.StronglyMeasurable g)
(hsm : MeasurableSet s)
(hs : μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (g x)))
:
MeasurableSet (MeasureTheory.Egorov.iUnionNotConvergentSeq hε hf hg hsm hs hfg)
theorem
MeasureTheory.Egorov.measure_iUnionNotConvergentSeq
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
[MetricSpace β]
{μ : MeasureTheory.Measure α}
{s : Set α}
{ε : ℝ}
{f : ι → α → β}
{g : α → β}
[SemilatticeSup ι]
[Nonempty ι]
[Countable ι]
(hε : 0 < ε)
(hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n))
(hg : MeasureTheory.StronglyMeasurable g)
(hsm : MeasurableSet s)
(hs : μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (g x)))
:
μ (MeasureTheory.Egorov.iUnionNotConvergentSeq hε hf hg hsm hs hfg) ≤ ENNReal.ofReal ε
theorem
MeasureTheory.Egorov.iUnionNotConvergentSeq_subset
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
[MetricSpace β]
{μ : MeasureTheory.Measure α}
{s : Set α}
{ε : ℝ}
{f : ι → α → β}
{g : α → β}
[SemilatticeSup ι]
[Nonempty ι]
[Countable ι]
(hε : 0 < ε)
(hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n))
(hg : MeasureTheory.StronglyMeasurable g)
(hsm : MeasurableSet s)
(hs : μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (g x)))
:
MeasureTheory.Egorov.iUnionNotConvergentSeq hε hf hg hsm hs hfg ⊆ s
theorem
MeasureTheory.Egorov.tendstoUniformlyOn_diff_iUnionNotConvergentSeq
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
[MetricSpace β]
{μ : MeasureTheory.Measure α}
{s : Set α}
{ε : ℝ}
{f : ι → α → β}
{g : α → β}
[SemilatticeSup ι]
[Nonempty ι]
[Countable ι]
(hε : 0 < ε)
(hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n))
(hg : MeasureTheory.StronglyMeasurable g)
(hsm : MeasurableSet s)
(hs : μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (g x)))
:
TendstoUniformlyOn f g Filter.atTop (s \ MeasureTheory.Egorov.iUnionNotConvergentSeq hε hf hg hsm hs hfg)
theorem
MeasureTheory.tendstoUniformlyOn_of_ae_tendsto
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
[MetricSpace β]
{μ : MeasureTheory.Measure α}
[SemilatticeSup ι]
[Nonempty ι]
[Countable ι]
{f : ι → α → β}
{g : α → β}
{s : Set α}
(hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n))
(hg : MeasureTheory.StronglyMeasurable g)
(hsm : MeasurableSet s)
(hs : μ s ≠ ⊤)
(hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (g x)))
{ε : ℝ}
(hε : 0 < ε)
:
∃ t ⊆ s, MeasurableSet t ∧ μ t ≤ ENNReal.ofReal ε ∧ 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 : MeasurableSpace α}
[MetricSpace β]
{μ : MeasureTheory.Measure α}
[SemilatticeSup ι]
[Nonempty ι]
[Countable ι]
{f : ι → α → β}
{g : α → β}
[MeasureTheory.IsFiniteMeasure μ]
(hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n))
(hg : MeasureTheory.StronglyMeasurable g)
(hfg : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (g x)))
{ε : ℝ}
(hε : 0 < ε)
:
∃ (t : Set α), MeasurableSet t ∧ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g Filter.atTop tᶜ
Egorov's theorem for finite measure spaces.