まずは数列の極限の証明を見て見ましょう。
$$\lim_{n\to\infty}n = \infty\hspace{20cm}$$
example : Tendsto (fun n:ℕ => n) atTop atTop := by
exact tendsto_id
exact一発で終わるということは全く同じか、より一般化された証明があるということです。この場合は少し一般化された定理tendsto_idがすでにmathlib4にあり、それが使われました。
tendsto_idという定理はFilter.tendsto_id.{u_1} {α : Type u_1} {x : Filter α} : Tendsto id x xです。要は恒等写像idの場合、定義域のフィルタと値域のフィルタは同じである、ということです。まあ恒等写像ですからそこに差は生じ得ませんね。我々の証明の対象はTendsto (fun n:ℕ => n) atTop atTopでした。fun n:ℕ => nは恒等写像ですし、第二引数と第三引数は同じですから、tendsto_idをx=atTopとして適用すれば証明は終了です。
$$\lim_{n\to\infty}2\,n = \infty\hspace{20cm}$$
example : Tendsto (fun n:ℕ => 2*n) atTop atTop := by
apply tendsto_atTop_atTop_of_monotone' (fun n m h => by linarith)
-- ⊢ ¬BddAbove (range fun n ↦ 2 * n)
rw[BddAbove,range,upperBounds,Set.Nonempty]
push_neg
intro B
rw [mem_setOf]
push_neg -- ⊢ ∃ a ∈ {x | ∃ y, 2 * y = x}, B < a
use 2*(B+1) -- ⊢ 2 * (B + 1) ∈ {x | ∃ y, 2 * y = x} ∧ B < 2 * (B + 1)
rw [mem_setOf] -- ⊢ (∃ y, 2 * y = 2 * (B + 1)) ∧ B < 2 * (B + 1)
constructor
· use B+1 -- ∃ y, 2 * y = 2 * (B + 1)の証明
linarith -- B < 2 * (B + 1)の証明
具体的には偶数列2, 4, 6, 8, …という数列は発散する、ということです。生成AIに聞くとapply tendsto_atTop_atTop_of_monotone' (fun n m h => by linarith)が使えるということだったので、１行目はそれにしました。
Filter.tendsto_atTop_atTop_of_monotone' (h : Monotone u) (H : ¬BddAbove (range u)) : Tendsto u atTop atTop
という定理は関数uが単調増加(monotone)でかつ上に有界(BddAbove)でないならば、定義域で無限大に行くと、値域でも無限大に行く、という意味になります。証明の最初の行では偶数列が単調増加であることの証明は証明項で与えられているので、残った「偶数列は上に有界でない」を意味する¬BddAbove (range fun n ↦ 2 * n)がゴールに残ります。
BddAboveの定義を使って展開しそこに現れるrange, upperBounds,Set.Nonemptyも定義に従って展開し、少々見やすくするとゴールは
∃ a ∈ {x | ∃ y, 2 * y = x}, B < a
という式になります。ここまでくればあとは以前に習った技を使えば簡単に証明が終了しました。
対象とする関数が恒等関数の場合は、あらかじめ証明されているtendsto_idを使って１行で証明が終わりましたが、偶数列の場合には結構面倒でした。これは個別具体的な数列を与えたため、その個別の性質を使った計算をせざる追えなかったからです。
次回は関数の極限の証明を見てみましょう。
