English
Under the same hypotheses, for any ε>0 there exists a j ∈ ι such that the measure of s ∩ notConvergentSeq f g n j is at most ε·2^{-n}. This gives a quantitative bound on the exceptional set.
Русский
При тех же предположениях для любого ε>0 существует j∈ι такое, что мера s ∩ notConvergentSeq f g n j не превосходит ε·2^{-n}. Это обеспечивает количественную оценку исключительной области.
LaTeX
$$$\exists j:\; μ(s ∩ notConvergentSeq f g n j) ≤ ε \cdot 2^{-n}$.$$
Lean4
theorem exists_notConvergentSeq_lt (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 : ℕ) :
∃ j : ι, μ (s ∩ notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * 2⁻¹ ^ n) :=
by
have ⟨N, hN⟩ :=
(ENNReal.tendsto_atTop ENNReal.zero_ne_top).1 (measure_notConvergentSeq_tendsto_zero hf hg hsm hs hfg n)
(.ofReal (ε * 2⁻¹ ^ n)) (by positivity)
rw [zero_add] at hN
exact ⟨N, (hN N le_rfl).2⟩
