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 #

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 : α} :
    x MeasureTheory.Egorov.notConvergentSeq f g n j kj, 1 / (n + 1) < dist (f k x) (g 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 sFilter.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 sFilter.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 sFilter.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 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.

    Equations
    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 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 : 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 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.

      Equations
      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 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 : 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 sFilter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (g x))) :
        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 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 : 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 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 : 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 sFilter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (g x))) {ε : } (hε : 0 < ε) :
        ts, 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.