English
There is a distinguished index notConvergentSeqLTIndex hε hf hg hsm hs hfg n such that the measure of s ∩ notConvergentSeq f g n at that index is bounded by ε·2^{-n}. This index is chosen according to the earlier bound.
Русский
Существует особый индекс notConvergentSeqLTIndex hε hf hg hsm hs hfg n, для которого мера s ∩ notConvergentSeq f g n ограничена ε·2^{-n}. Индекс выбирается так же, как и ранее.
LaTeX
$$$μ\bigl(s ∩ notConvergentSeq f g n (notConvergentSeqLTIndex hε hf hg hsm hs hfg n)\bigr) ≤ ε·2^{-n}$.$$
Lean4
theorem notConvergentSeqLTIndex_spec (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))) (n : ℕ) :
μ (s ∩ notConvergentSeq f g n (notConvergentSeqLTIndex hε hf hg hsm hs hfg n)) ≤ ENNReal.ofReal (ε * 2⁻¹ ^ n) :=
Classical.choose_spec <| exists_notConvergentSeq_lt hε hf hg hsm hs hfg n
