今回は関数の極限の証明を見ていきます。
$$\lim_{x\to 2} 2\,x = 4\hspace{20cm}$$
example : Tendsto (fun x:ℝ => 2*x) (𝓝 2) (𝓝 4) := by
have cont_two_mul : Continuous (fun x : ℝ => 2 * x) := by
exact continuous_const.mul continuous_id
refine Continuous.tendsto' cont_two_mul 2 4 ?h -- ⊢ 2 * 2 = 4
linarith
証明するべきことは引数を２倍にする関数$x\mapsto2\,x$で$x\to 2$の時$2\,x\to 4$になるという式です。Tendstoとフィルタを使った記述も案外見やすいですね。
証明はまずひとつの補題の証明から始まります。それは関数$x\mapsto2\,x$は連続である、という補題です。証明は１行で終わっていて、恒等関数$x\mapsto x$は連続であるという定理と、連続関数に定数をかけても連続である、という定理を使っています。いずれもmathlib4で証明済みです。
mathlib4にはさらに定理「連続関数$f(x)$では$\lim_{x\to a}f(x)= f(a)$」という定理が証明済みです。この定理を使ってゴールを整理すると、$f(2)=4$が最後に証明するべきゴールになります。ここで関数が$x\mapsto2\,x$ですから$2\cdot 2=4$がゴールになります。このような簡単な式の計算だけが残った場合linarithを使って証明が終了します。
偶数列が発散する場合の証明とこの証明は、ゴールは似ていますが手法は全く異なります。関数の極限ではcontinuous_const.mul, continuous_id, Continuous.tendts_to'などの道具が整備されていて、それらを使いこなすことで簡単に証明が終わりました。
$$\lim_{x\to \infty} \frac1{x} = 0\hspace{20cm}$$
example : Tendsto (fun x:ℝ => 1/x) atTop (𝓝 0) := by
refine Metric.tendsto_atTop.mpr ?_ -- ⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (1 / n) 0 < ε
intro ε h1 -- ⊢ ∃ N, ∀ n ≥ N, dist (1 / n) 0 < ε
use 2/ε -- ⊢ ∀ n ≥ 2 / ε, dist (1 / n) 0 < ε
intro d h2 -- ⊢ dist (1 / d) 0 < ε
simp -- ⊢ |d|⁻¹ < ε
have h3 : 2≤ε*d := by exact (div_le_iff₀' h1).mp h2
have h4 : 0<d := by
have : 0<2/ε := by
refine (div_pos_iff_of_pos_right h1).mpr ?_; linarith
linarith
have h5 : |d|=d := by exact abs_of_pos h4
rw [h5] -- ⊢ d⁻¹ < ε
refine (inv_lt_iff_one_lt_mul₀ h4).mpr ?_ -- ⊢ 1 < ε * d
linarith
次はもう少し中身のあるやつです。$\lim_{x\to \infty} \frac1{x} = 0$を証明します。
証明はrefine Metric.tendsto_atTop.mpr ?_という行で始まります。Metric.tendsto_atTopは定理で、Filter.Tendstoによる極限はいわゆる$\varepsilon - \delta$論法と同値であることを述べています。そしてrefineを使うことでゴールをTendstoとフィルタから$\varepsilon - \delta$論法の形に変換できます。その結果ゴールは、
∀ ε > 0, ∃ N, ∀ n ≥ N, dist (1 / n) 0 < ε
になります。
次の intro ε h1 でε:Rが仮定に入りさらに h1:ε>0も仮定に入ります。ゴールは
∃ N, ∀ n ≥ N, dist (1 / n) 0 < ε
となります。
存在量化子のついたNに2/εを入れれば証明はうまくいくはず、なのでuse 2/εを使いました。これでゴールは、
∀ n ≥ 2 / ε, dist (1 / n) 0 < ε
となります。
intro d h2でnをdと書き換えてd:Rとh2:d≥ 2 / εが仮定に入ります。ゴールは
dist (1 / d) 0 < ε
となります。
次のsimpでdistが展開されました。ゴールは、
|d|⁻¹ < ε
となりました。この式をh1:ε>0, h2:d≥ 2 / εを使って証明します。まずサクッとh3:2≤ε*dを証明します。またh4:0<dもサクッと証明します。このh４を使えばh5:|d|=dが言えるのでこれを使ってrw [h5]でゴールの絶対値を外します。ゴールは、
d⁻¹ < ε
です。ここからほぼ自明に1 < ε * d です。既にh3:2≤ε*dを証明してありますから、1<2≤ε*dから証明は終了します。最後のステップは簡単な不等号計算ですからlinarithがやってくれました。
$\lim_{x\to \infty} \frac1{x} = 0$の証明ではtendstoとフィルタを普通の$\varepsilon - \delta$に展開して、適当にdをεで表して普通のやり方で証明しました。
