具体的な極限計算¶
実数列 \(a_n\) が \(+\infty\) に発散することは，Lean では
と書きます．
たとえば，自然数を実数に埋め込んだ列 \(n \mapsto n\) は atTop に収束します．
具体的な極限計算では，次の 2 つを分けると読みやすくなります．
Continuous.tendstoなどで，まずTendstoの証明を作る．- 終点の値の計算は
calcで段階的に書く．
calc は，等式や不等式を紙の計算に近い形で並べるための構文です．
Tendsto そのものを calc で示すというより，
𝓝 ((3 : ℝ)^2 + 1) を 𝓝 10 に直すような小さな計算に使うと効果的です．
section ConcreteLimits
example : Tendsto (fun n : ℕ => (n : ℝ)) atTop atTop := by
exact tendsto_natCast_atTop_atTop
一点での関数の極限は，始域側を 𝓝 a，終域側を 𝓝 b として
と書きます．
以下は \(\lim_{x \to 2} (x+3) = 5\) です．
Continuous.tendsto は，連続性からその点での極限を取り出す補題です．
最後に，2 + 3 = 5 という数値計算を calc で明示します．
example : Tendsto (fun x : ℝ => x + 3) (𝓝 2) (𝓝 5) := by
have hlim :
Tendsto (fun x : ℝ => x + 3) (𝓝 2) (𝓝 ((2 : ℝ) + 3)) :=
((by continuity : Continuous fun x : ℝ => x + 3).tendsto (2 : ℝ))
have hval : (2 : ℝ) + 3 = 5 := by
calc
(2 : ℝ) + 3 = (5 : ℝ) := by norm_num
_ = 5 := by rfl
simpa [hval] using hlim
上の例では，連続性から得られる極限はまず
という形です．
一方，示したいゴールは終域側が 𝓝 5 です．
そこで，まずこの極限を hlim として保存し，値の計算
を hval として別に示します．
最後の simpa [hval] using hlim は，hlim の終域側の 𝓝 (2 + 3) を
𝓝 5 に書き換えています．
同じ方針で，多項式や初等関数の極限も計算できます． 次は \(\lim_{x \to 3} (x^2+1) = 10\) と \(\lim_{x \to 0}(\sin x + x^2)=0\) です．
example : Tendsto (fun x : ℝ => x ^ 2 + 1) (𝓝 3) (𝓝 10) := by
have hlim :
Tendsto (fun x : ℝ => x ^ 2 + 1) (𝓝 3) (𝓝 ((3 : ℝ) ^ 2 + 1)) :=
((by continuity : Continuous fun x : ℝ => x ^ 2 + 1).tendsto (3 : ℝ))
have hval : (3 : ℝ) ^ 2 + 1 = 10 := by
calc
(3 : ℝ) ^ 2 + 1 = (9 : ℝ) + 1 := by norm_num
_ = 10 := by norm_num
simpa [hval] using hlim
収束先の値を明示しない方法¶
収束先の値をまだ計算したくないときは，𝓝 10 のように数値を明示せず，
𝓝 (f a) の形で書けます．
たとえば次の例は，\(\lim_{x \to 3}(x^2+1)\) の値を 10 まで計算せず，
単に「点 3 における関数値」へ収束する，という形で述べています．
example :
Tendsto (fun x : ℝ => x ^ 2 + 1) (𝓝 3)
(𝓝 ((fun x : ℝ => x ^ 2 + 1) 3)) := by
exact ((by continuity : Continuous fun x : ℝ => x ^ 2 + 1).tendsto (3 : ℝ))
より一般に，収束先の値そのものを命題の外に出したいなら， 存在命題として
と書けます．
この場合，証明の中では refine ⟨..., ?_⟩ によって候補となる値を与えます．
example :
∃ y : ℝ, Tendsto (fun x : ℝ => x ^ 2 + 1) (𝓝 3) (𝓝 y) := by
refine ⟨(fun x : ℝ => x ^ 2 + 1) 3, ?_⟩
exact ((by continuity : Continuous fun x : ℝ => x ^ 2 + 1).tendsto (3 : ℝ))
一方で，statement に直接 𝓝 _ と書いて収束先を完全に空欄にする方法は，
通常はうまくいきません．
-- これは基本的には失敗します．
-- example : Tendsto (fun x : ℝ => x ^ 2 + 1) (𝓝 3) (𝓝 _) := by
-- exact ((by continuity : Continuous fun x : ℝ => x ^ 2 + 1).tendsto (3 : ℝ))
example : ... の型は証明本体を読む前に確定されるため，
証明本体から _ の中身を推論することはできないからです．
値を計算したくない場合は，まず 𝓝 (f a) の形で書くのが実用的です．
example : Tendsto (fun x : ℝ => Real.sin x + x ^ 2) (𝓝 0) (𝓝 0) := by
simpa using ((by continuity : Continuous fun x : ℝ => Real.sin x + x ^ 2).tendsto (0 : ℝ))
無限遠での極限も同じ Tendsto です．
次は \(\lim_{x \to +\infty} 1/x = 0\) です．
ここでは始域側のフィルターが atTop，終域側のフィルターが 𝓝 0 になっています．