English
If μ is finite, each f_n is strongly measurable, g is strongly measurable, and f_n(x) converges to g(x) almost everywhere, then f converges to g in measure along atTop.
Русский
Если μ конечна, каждый f_n измерим по мере сильно, g тоже сильно измерима, и для почти всех x выполняется сходящаяся последовательность f_n(x) → g(x), то f сходится по мере к g вдоль atTop.
LaTeX
$$$[IsFiniteMeasure\;\mu] \;\big(\forall n,\; StronglyMeasurable(f_n)\big) \;\to\; (StronglyMeasurable(g)) \\to\; (\forall^{\;x\;}(\mu\text{-a.e.})\ Tendsto (f_n(x))\ to\ g(x)) \\Rightarrow\; TendstoInMeasure\;\mu\;f\;atTop\;g$$
Lean4
/-- Auxiliary lemma for `tendstoInMeasure_of_tendsto_ae`. -/
theorem tendstoInMeasure_of_tendsto_ae_of_stronglyMeasurable [IsFiniteMeasure μ] (hf : ∀ n, StronglyMeasurable (f n))
(hg : StronglyMeasurable g) (hfg : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))) :
TendstoInMeasure μ f atTop g :=
by
refine fun ε hε => ENNReal.tendsto_atTop_zero.mpr fun δ hδ => ?_
by_cases hδi : δ = ∞
· simp only [hδi, imp_true_iff, le_top, exists_const]
lift δ to ℝ≥0 using hδi
rw [gt_iff_lt, ENNReal.coe_pos, ← NNReal.coe_pos] at hδ
obtain ⟨t, _, ht, hunif⟩ := tendstoUniformlyOn_of_ae_tendsto' hf hg hfg hδ
rw [ENNReal.ofReal_coe_nnreal] at ht
rw [EMetric.tendstoUniformlyOn_iff] at hunif
obtain ⟨N, hN⟩ := eventually_atTop.1 (hunif ε hε)
refine ⟨N, fun n hn => ?_⟩
suffices {x : α | ε ≤ edist (f n x) (g x)} ⊆ t from (measure_mono this).trans ht
rw [← Set.compl_subset_compl]
intro x hx
rw [Set.mem_compl_iff, Set.notMem_setOf_iff, edist_comm, not_le]
exact hN n hn x hx
