MeasureTheory.tendstoUniformlyOn_of_ae_tendsto'
theorem MeasureTheory.tendstoUniformlyOn_of_ae_tendsto' :
∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [inst : MetricSpace β]
{μ : MeasureTheory.Measure α} [inst_1 : SemilatticeSup ι] [inst_2 : Nonempty ι] [inst_3 : Countable ι]
{f : ι → α → β} {g : α → β} [inst_4 : MeasureTheory.IsFiniteMeasure μ],
(∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)) →
MeasureTheory.StronglyMeasurable g →
(∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
∀ {ε : ℝ},
0 < ε → ∃ t, MeasurableSet t ∧ ↑↑μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g Filter.atTop tᶜ
Egorov's theorem for finite measure spaces states that given a finite measure space and a sequence of strongly measurable functions `f : ι → α → β` that almost everywhere converge to a strongly measurable function `g : α → β`, for every positive real number `ε`, there exists a measurable set `t` such that the measure of `t` is less than or equal to `ε` and the sequence of functions `f` converges uniformly to `g` outside `t`. The notion of convergence used here is: for every neighborhood of `g(x)`, for large enough `n`, `f(n, x)` lies in that neighborhood. Strong measurability of a function implies that it can be approximated pointwise by a sequence of simple functions. The theorem thus describes a trade-off between how closely the functions `f(n, x)` approximate `g(x)`, and the measure of the set where the approximation is worst.
More concisely: Given a finite measure space and a sequence of strongly measurable functions converging almost everywhere to a limit function, there exists a set of measure less than any given positive number such that the sequence converges uniformly to the limit outside this set.
|
MeasureTheory.tendstoUniformlyOn_of_ae_tendsto
theorem MeasureTheory.tendstoUniformlyOn_of_ae_tendsto :
∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [inst : MetricSpace β]
{μ : MeasureTheory.Measure α} [inst_1 : SemilatticeSup ι] [inst_2 : Nonempty ι] [inst_3 : Countable ι]
{f : ι → α → β} {g : α → β} {s : Set α},
(∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)) →
MeasureTheory.StronglyMeasurable g →
MeasurableSet s →
↑↑μ s ≠ ⊤ →
(∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
∀ {ε : ℝ},
0 < ε →
∃ t ⊆ s, MeasurableSet t ∧ ↑↑μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g Filter.atTop (s \ t)
**Egorov's theorem**: Given a countable sequence of strongly measurable functions `f : ι → α → β` that converges to a function `g : α → β` almost everywhere on a finite-measure, measurable set `s`, Egorov's theorem states that for any real number `ε > 0`, there exists a subset `t` of `s`, with `μ t ≤ ε`, such that the function sequence `f` converges uniformly to `g` on the set difference `s \ t`. This implies that a sequence of functions that converges almost everywhere can be made to converge uniformly, except on an arbitrarily small set. The index type `ι` of the function sequence is required to be countable and usually set to be the natural numbers `ℕ`.
More concisely: Given a countable sequence of strongly measurable functions from a measurable set to a metric space that converges almost everywhere to a limit function on a finite-measure set, there exists a subset of arbitrarily small measure where the sequence converges uniformly to the limit.
|