English
In a finite-measure space, there exists a measurable set t of arbitrarily small measure such that f converges uniformly to g outside t.
Русский
На пространстве с конечной мерой существует измеримое множество t с произвольно малой мерой, такое что вне t f сходится единообразно к g.
LaTeX
$$$\exists t, MeasurableSet t ∧ μ t ≤ ε ∧ TendstoUniformlyOn f g atTop (Set.univ \ t)$.$$
Lean4
/-- Egorov's theorem for finite measure spaces. -/
theorem tendstoUniformlyOn_of_ae_tendsto' [IsFiniteMeasure μ] (hf : ∀ n, StronglyMeasurable (f n))
(hg : StronglyMeasurable g) (hfg : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))) {ε : ℝ} (hε : 0 < ε) :
∃ t, MeasurableSet t ∧ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ :=
by
have ⟨t, _, ht, htendsto⟩ :=
tendstoUniformlyOn_of_ae_tendsto hf hg MeasurableSet.univ (measure_ne_top μ Set.univ)
(by filter_upwards [hfg] with _ htendsto _ using htendsto) hε
refine ⟨_, ht, ?_⟩
rwa [Set.compl_eq_univ_diff]
