極限湯與大歐 Reprise

證了一個主要定理，列了三個 lemmas，對於 big-O 的相關證明應該很有用。其中對一般人特別有用的應該是第一個 lemma：如果普通的極限存在，lim sup 和 lim inf 就會等於那個極限值，這時就只需要操作一般的 limits。第二個 lemma 對（去年的）隨機客是 big-Omega 的定義。Little-o 和 little-omega 等其他符號也可以用極限處理，這在 Wikipedia 上有整理出來。不過原則都是一樣的，其實用 lim sup 就可以處理全部情形了。

簡單描述一下定理的證明。Only if 的部份是 trivial。If 的部份，lim sup 的直覺定義是最大凝聚點，所以從這點的右邊一點點（\alpha + \varepsilon）切下去，更右邊的點頂多 finite。把這些點排除後，剩下連續一串無窮的點值都會小於 \alpha + \varepsilon。取 n₀ 為這串的起頭位置，c 為 \alpha + \varepsilon 就完了。

順帶提供科普小常識：如果你覺得我現在做的事情很像釋出寫好的程式，這感覺就是 Curry-Howard isomorphism。定理的命題敘述就是函式的型別（propositions as types），定理的證明就是函式的實作（proofs as programs）。所以你當然也可以把定理當作黑盒子來用，不看它的實作。不過 principle of abstraction 並不是叫我們不要看函式實作，而是在用的時候選擇性忽略之，能看一次實作還是最好 XD。

--
有這些 lemmas，AI 作業的分析應該就沒問題了 XD。