book集

section 主定理
word ap
txt \(s(n)\) を初項 \(a\)、公比 \(r\) の等比数列の最初の \(n\) 項の和 \(a + ar + \cdots + ar^{n-1}\) とします。
txt ここでは \(s\) を \(s(0) = 0\) と漸化式 \(s(i+1) = s(i) + ar^i\) を満たす関数として仮定します（\(a\)・\(r\) は自然数）。そのような \(s\) が存在することは示しません。したがって主定理は「そのような \(s\) があれば」という条件付きの形です（\(s\) が無ければ何も言っていません）。
txt 自然数には引き算が無いので、\((r-1)\,s(n) = a(r^n - 1)\) を両辺に \(s(n) + a\) を足した形 \(r\,s(n) + a = s(n) + ar^n\) で述べます（\(r = 1\) のときは \(s(n) = na\) を言わない点に注意）。
txt 証明は \(n\) についての帰納法です。\(n = 0\) では両辺とも \(a\)。\(n\) から \(n+1\) へは \(r\,s(n+1) + a = (r\,s(n) + a) + ar^{n+1} = s(n) + ar^n + ar^{n+1} = s(n+1) + ar^{n+1}\)。
thm `\\{ And [ a ; r col ∈ 𝕄 ] \\ s ap (0) = 0 \\ [ ∀ i ∈ 𝕄 . s ap (i suc) = s ap (i) + a ⋅ r ↑ i ] \\} and n ∈ 𝕄 ⟹ r ⋅ s ap (n) + a = s ap (n) + a ⋅ r ↑ n` ◀ 𝕄0s , IND𝕄 , +𝕄 , *𝕄 , ↑𝕄 , 1.
prf hy1 <- `[ |a ; |r col ∈ 𝕄 ]` ;
    hy0 <- `|s ap (0) = 0` ;
    hyS <- `[ ∀ i ∈ 𝕄 . |s ap (i suc) = |s ap (i) + |a ⋅ |r ↑ i ]` ;
    L∈ <- `n ∈ 𝕄 ⟹ |s ap (n) ∈ 𝕄` -| IND𝕄[C_:=`\{ cls n | |s ap (n) ∈ 𝕄 \}`] , hy0 , hyS , hy1 , 𝕄0s , +∈𝕄 , ⋅∈𝕄 , ↑∈𝕄 v;
    Lb <- `|r ⋅ |s ap (0) + |a = |s ap (0) + |a ⋅ |r ↑ 0` -| hy0 , hy1 , ↑𝕄 , *𝕄 , L0+ , L⋅1 , +𝕄 , 𝕄0s p;
    hyM <- `|m ∈ 𝕄` ;
    hyI <- `|r ⋅ |s ap (|m) + |a = |s ap (|m) + |a ⋅ |r ↑ |m` ;
    F1 <- `|r ⋅ |s ap (|m suc) = |r ⋅ |s ap (|m) + |r ⋅ (|a ⋅ |r ↑ |m)` -| hyS , hyM , Ldist , L∈ , hy1 , ⋅∈𝕄 , ↑∈𝕄 v;
    F2 <- `|r ⋅ (|a ⋅ |r ↑ |m) = |a ⋅ |r ↑ { |m suc }` -| ↑𝕄 , ⋅A , ⋅C , hy1 , hyM , ↑∈𝕄 , ⋅∈𝕄 v;
    E1 <- `|r ⋅ |s ap (|m suc) + |a = (|r ⋅ |s ap (|m) + |a) + |a ⋅ |r ↑ { |m suc }` -| F1 , F2 , +A , +C , +∈𝕄 , ⋅∈𝕄 , L∈ , ↑∈𝕄 , hy1 , hyM , 𝕄0s v;
    Ls1 <- `|r ⋅ |s ap (|m suc) + |a = |s ap (|m suc) + |a ⋅ |r ↑ { |m suc }` -| E1 , hyI , hyS , hy1 , hyM , L∈ , +A , +∈𝕄 , ⋅∈𝕄 , ↑∈𝕄 v;
    Ls <- `[ a ; r col ∈ 𝕄 ] and s ap (0) = 0 and [ ∀ i ∈ 𝕄 . s ap (i suc) = s ap (i) + a ⋅ r ↑ i ] and m ∈ 𝕄 and r ⋅ s ap (m) + a = s ap (m) + a ⋅ r ↑ m ⟹ r ⋅ s ap (m suc) + a = s ap (m suc) + a ⋅ r ↑ { m suc }` -| 𝕄0s , IND𝕄 , +𝕄 , *𝕄 , ↑𝕄 , 1. h[fix];
    hyN <- `|n ∈ 𝕄` ;
    Lfix <- `|r ⋅ |s ap (|n) + |a = |s ap (|n) + |a ⋅ |r ↑ |n` -| IND𝕄[C_:=`\{ cls n | |r ⋅ |s ap (n) + |a = |s ap (n) + |a ⋅ |r ↑ n \}`] , Lb , Ls , hyN , hy1 , hy0 , hyS v;
    goal -| 𝕄0s , IND𝕄 , +𝕄 , *𝕄 , ↑𝕄 , 1. h[fix];

articles3/66.book

`articles3/66.book`