English
If f: β → ENNReal is antitone, then Tendsto f atTop (nhds 0) is equivalent to: for every ε > 0, there exists n with f(n) < ε.
Русский
Если f: β → ENNReal анти́монотоневая, то сходимость f к 0 при atTop эквивалентна тому, что для каждого ε > 0 существует n, такое что f(n) < ε.
LaTeX
$$$\\\\text{Antitone } f \\\\Rightarrow \\\\operatorname{Tendsto} f \\\\mathrm{atTop} \\\\,(\\\\mathit{nhds} \ 0) \\\\iff \\\\forall \\\\varepsilon > 0, \\\\exists n: f(n) < \\\\varepsilon.$$$
Lean4
theorem tendsto_atTop_zero_iff_lt_of_antitone {β : Type*} [Nonempty β] [SemilatticeSup β] {f : β → ℝ≥0∞}
(hf : Antitone f) : Filter.Tendsto f Filter.atTop (𝓝 0) ↔ ∀ ε, 0 < ε → ∃ n : β, f n < ε :=
by
rw [ENNReal.tendsto_atTop_zero_iff_le_of_antitone hf]
constructor <;> intro h ε hε
· obtain ⟨n, hn⟩ :=
h (min 1 (ε / 2)) (lt_min_iff.mpr ⟨zero_lt_one, (ENNReal.div_pos_iff.mpr ⟨ne_of_gt hε, ENNReal.ofNat_ne_top⟩)⟩)
· refine ⟨n, hn.trans_lt ?_⟩
by_cases hε_top : ε = ∞
· rw [hε_top]
exact (min_le_left _ _).trans_lt ENNReal.one_lt_top
refine (min_le_right _ _).trans_lt ?_
rw [ENNReal.div_lt_iff (Or.inr hε.ne') (Or.inr hε_top)]
conv_lhs => rw [← mul_one ε]
rw [ENNReal.mul_lt_mul_left hε.ne' hε_top]
simp
· obtain ⟨n, hn⟩ := h ε hε
exact ⟨n, hn.le⟩
