English
Egorov’s theorem for almost everywhere convergence: from ae convergence on s with finite measure to uniform convergence on s\t after discarding a small measurable t.
Русский
Егоров для почти везде сходящейся: из ae-сходимости на s получаем единообразную на s\t после удаления малого измеримого множества.
LaTeX
$$$\exists t \subseteq s,\; MeasurableSet t \land μ t ≤ ε \land TendstoUniformlyOn f g atTop (s \ t)$.$$
Lean4
/-- **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 tendstoUniformlyOn_of_ae_tendsto (hf : ∀ n, StronglyMeasurable (f n)) (hg : StronglyMeasurable g)
(hsm : MeasurableSet s) (hs : μ s ≠ ∞) (hfg : ∀ᵐ x ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))) {ε : ℝ}
(hε : 0 < ε) : ∃ t ⊆ s, MeasurableSet t ∧ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (s \ t) :=
⟨Egorov.iUnionNotConvergentSeq hε hf hg hsm hs hfg, Egorov.iUnionNotConvergentSeq_subset hε hf hg hsm hs hfg,
Egorov.iUnionNotConvergentSeq_measurableSet hε hf hg hsm hs hfg,
Egorov.measure_iUnionNotConvergentSeq hε hf hg hsm hs hfg,
Egorov.tendstoUniformlyOn_diff_iUnionNotConvergentSeq hε hf hg hsm hs hfg⟩
