English
The difference between the two side convergences tends uniformly on the complement of the union of notConvergentSeq.
Русский
Разность между пределами сходится единообразно на дополнении объединения notConvergentSeq.
LaTeX
$$$TendstoUniformlyOn f g atTop (\text{Set.univ} \ Egorov.iUnionNotConvergentSeq hε hf hg hsm hs hfg)$.$$
Lean4
theorem tendstoUniformlyOn_diff_iUnionNotConvergentSeq (hε : 0 < ε) (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))) :
TendstoUniformlyOn f g atTop (s \ Egorov.iUnionNotConvergentSeq hε hf hg hsm hs hfg) :=
by
rw [EMetric.tendstoUniformlyOn_iff]
intro δ hδ
obtain ⟨N, hN⟩ := ENNReal.exists_inv_nat_lt hδ.ne'
rw [eventually_atTop]
refine ⟨Egorov.notConvergentSeqLTIndex (half_pos hε) hf hg hsm hs hfg N, fun n hn x hx => ?_⟩
simp only [Set.mem_diff, Egorov.iUnionNotConvergentSeq, not_exists, Set.mem_iUnion, Set.mem_inter_iff, not_and,
exists_and_left] at hx
obtain ⟨hxs, hx⟩ := hx
specialize hx hxs N
rw [Egorov.mem_notConvergentSeq_iff] at hx
push_neg at hx
rw [edist_comm]
exact lt_of_le_of_lt (hx n hn) hN
