今日は3月14日、毎年恒例の円周率の日です。 今年はなんと満月なんです。今、まだ今夜の満月を見ていない人、すぐに外に出てください。関東地方は晴れていて見られます。 記念に今夜のお月様を撮って見ました。次に円周率の日に満月が見られるのはいつのこと…

少し複雑な関数の極限として $$\lim_{x\to 0}x\,\sin{\frac1{x}}=0$$ を証明します。$x$が$\sin$の引数の分母にあるので$x=0$では定義されませんが$x\to 0$での極限は存在して$0$になる、という命題です。 今回は関数の絶対値を取ってから挟み撃ち論法で証明…

今回は関数の極限の証明を見ていきます。 $$\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 C…

まずは数列の極限の証明を見て見ましょう。 $$\lim_{n\to\infty}n = \infty\hspace{20cm}$$ example : Tendsto (fun n:ℕ => n) atTop atTop := by exact tendsto_id exact一発で終わるということは全く同じか、より一般化された証明があるということです。こ…

Mathematics in Lean 4も最後の方に辿り着きつつあります。これから数回にわたってLean4による解析学の証明を見ていきます。Mathematics In Lean 4の章立てで言えば10.1 Filtersあたりなのですが、そこでの扱いはもっとはるかに抽象的です。この記事では具体…