book集

section 二項係数
word choose
prop choose𝕄 <- `\\{ And n ∈ 𝕄 ⟹ n choose 0 = 1 \\ k ∈ 𝕄 ⟹ 0 choose (k suc) = 0 \\ [ n ; k col ∈ 𝕄 ] ⟹ (n suc) choose (k suc) = n choose k + n choose (k suc) \\}`
let/thm choose∈𝕄 <- `[ n ; k col ∈ 𝕄 ] ⟹ n choose k ∈ 𝕄` ◀ 𝕄0s , IND𝕄 , +𝕄 , choose𝕄 , 1.
prf Lb <- `[ ∀ k ∈ 𝕄 . 0 choose k ∈ 𝕄 ]` -| choose𝕄 , Lpred , 𝕄0s , `1 ∈ 𝕄` p;
    Ls <- `n ∈ 𝕄 and [ ∀ k ∈ 𝕄 . n choose k ∈ 𝕄 ] ⟹ [ ∀ k ∈ 𝕄 . (n suc) choose k ∈ 𝕄 ]` -| choose𝕄 , Lpred , +∈𝕄 , 𝕄0s , `1 ∈ 𝕄` v;
    choose∈𝕄 -| IND𝕄[C_:=`\{ cls n | [ ∀ k ∈ 𝕄 . n choose k ∈ 𝕄 ] \}`] , Lb , Ls , 𝕄0s v;
    choose∈𝕄 -| 𝕄0s , IND𝕄 , +𝕄 , choose𝕄 , 1. h;
!let/thm Lnn <- `n ∈ 𝕄 ⟹ n choose n = 1` ◀ 𝕄0s , IND𝕄 , +𝕄 , choose𝕄 , 1.
prf Lzb <- `[ ∀ k ∈ 𝕄 . 0 choose (0 + k suc) = 0 ]` -| choose𝕄 , L0+ , 𝕄0s p;
    Lzs <- `n ∈ 𝕄 and [ ∀ k ∈ 𝕄 . n choose (n + k suc) = 0 ] ⟹ [ ∀ k ∈ 𝕄 . (n suc) choose ((n suc) + k suc) = 0 ]` -| choose𝕄 , Lsuc+ , +𝕄 , +∈𝕄 , 𝕄0s v;
    Lz <- `[ n ; k col ∈ 𝕄 ] ⟹ n choose (n + k suc) = 0` -| IND𝕄[C_:=`\{ cls n | [ ∀ k ∈ 𝕄 . n choose (n + k suc) = 0 ] \}`] , Lzb , Lzs , 𝕄0s v;
    Ls <- `n ∈ 𝕄 and n choose n = 1 ⟹ (n suc) choose (n suc) = 1` -| choose𝕄 , Lz , +𝕄 , 𝕄0s , `1 ∈ 𝕄` v;
    Lnn -| IND𝕄[C_:=`\{ cls n | n choose n = 1 \}`] , choose𝕄 , Ls , 𝕄0s v;
    Lnn -| 𝕄0s , IND𝕄 , +𝕄 , choose𝕄 , 1. h;

newpage
section 主定理
word ap
txt \(s(n)(m)\) を \(\sum_{k\lt m} \binom{n}{k} a^k b^{n-k}\) とします。自然数には引き算が無いので、\(k + j = n\) と書いて \(b^{n-k}\) を \(b^j\) で表し、\(s\) を \(s(n)(0) = 0\) と漸化式 \(s(k+j)(k+1) = s(k+j)(k) + \binom{k+j}{k} a^k b^j\) を満たす関数として仮定します（存在は示しません）。したがって主定理は「そのような \(s\) があれば」という条件付きの形です（\(s\) が無ければ何も言っていません）。
txt 証明の要は \(s(n+1)(m+1) = b\,s(n)(m+1) + a\,s(n)(m)\)（\(m \le n\)・パスカルの漸化式から \(m\) についての帰納法）です。
thm `\\{ And [ a ; b col ∈ 𝕄 ] \\ [ ∀ n ∈ 𝕄 . s ap (n) ap (0) = 0 ] \\ [ ∀ k ∈ 𝕄 . [ ∀ j ∈ 𝕄 . s ap (k + j) ap (k suc) = s ap (k + j) ap (k) + ((k + j) choose k) ⋅ (a ↑ k ⋅ b ↑ j) ] ] \\} and n ∈ 𝕄 ⟹ (a + b) ↑ n = s ap (n) ap (n suc)` ◀ 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , ↑𝕄 , choose𝕄 , 1.
prf hy1 <- `[ |a ; |b col ∈ 𝕄 ]` ;
    hy0 <- `[ ∀ n ∈ 𝕄 . |s ap (n) ap (0) = 0 ]` ;
    hyR <- `[ ∀ k ∈ 𝕄 . [ ∀ j ∈ 𝕄 . |s ap (k + j) ap (k suc) = |s ap (k + j) ap (k) + ((k + j) choose k) ⋅ (|a ↑ k ⋅ |b ↑ j) ] ]` ;
    LT∈ <- `[ k ; j col ∈ 𝕄 ] ⟹ ((k + j) choose k) ⋅ (|a ↑ k ⋅ |b ↑ j) ∈ 𝕄` -| choose∈𝕄 , ↑∈𝕄 , ⋅∈𝕄 , +∈𝕄 , hy1 p;
    LS∈ <- `[ k ; j col ∈ 𝕄 ] ⟹ |s ap (k + j) ap (k) ∈ 𝕄` -| IND𝕄[C_:=`\{ cls k | [ ∀ j ∈ 𝕄 . |s ap (k + j) ap (k) ∈ 𝕄 ] \}`] , hy0 , hyR , LT∈ , L0+ , Lsuc+ , +𝕄 , +∈𝕄 , 𝕄0s v;
    B1 <- `j ∈ 𝕄 ⟹ |s ap (0 + j) ap (0 suc) = |b ↑ j` -| hyR , hy0 , hy1 , choose𝕄 , ↑𝕄 , L0+ , L⋅1 , ⋅C , ↑∈𝕄 , +∈𝕄 , 𝕄0s , `1 ∈ 𝕄` v;
    Kb <- `j ∈ 𝕄 ⟹ |s ap ((0 + j) suc) ap (0 suc) = |b ⋅ |s ap (0 + j) ap (0 suc) + |a ⋅ |s ap (0 + j) ap (0)` -| B1 , hy0 , hy1 , ↑𝕄 , ⋅C , *𝕄 , +𝕄 , L0+ , ↑∈𝕄 , ⋅∈𝕄 , +∈𝕄 , 𝕄0s v;
    A1a <- `[ b ; d ; p ; a ; q col ∈ 𝕄 ] ⟹ b ⋅ (d ⋅ ((p ⋅ a) ⋅ q)) = d ⋅ ((p ⋅ a) ⋅ (q ⋅ b))` -| ⋅A , ⋅C , ⋅∈𝕄 v;
    A1b <- `[ a ; c ; p ; q ; b col ∈ 𝕄 ] ⟹ a ⋅ (c ⋅ (p ⋅ (q ⋅ b))) = c ⋅ ((p ⋅ a) ⋅ (q ⋅ b))` -| ⋅A , ⋅C , ⋅∈𝕄 v;
    A1c <- `[ x ; y ; u ; v ; a ; b col ∈ 𝕄 ] ⟹ b ⋅ (x + u) + a ⋅ (y + v) = (b ⋅ x + a ⋅ y) + (a ⋅ v + b ⋅ u)` -| Ldist , +A , +C , ⋅∈𝕄 , +∈𝕄 v;
    A0 <- `[ x ; y ; c ; d ; a ; b ; t ; u ; v col ∈ 𝕄 ] and b ⋅ u = d ⋅ t and a ⋅ v = c ⋅ t ⟹ b ⋅ (x + u) + a ⋅ (y + v) = (b ⋅ x + a ⋅ y) + (c ⋅ t + d ⋅ t)` -| A1c , ⋅∈𝕄 v;
    A1 <- `[ x ; y ; c ; d ; a ; b ; p ; q col ∈ 𝕄 ] ⟹ (b ⋅ x + a ⋅ y) + (c + d) ⋅ ((p ⋅ a) ⋅ (q ⋅ b)) = b ⋅ (x + d ⋅ ((p ⋅ a) ⋅ q)) + a ⋅ (y + c ⋅ (p ⋅ (q ⋅ b)))` -| A0 , Rdist , A1a , A1b , ⋅∈𝕄 v;
    I1 <- `[ m ; j col ∈ 𝕄 ] ⟹ (m suc) + j = m + j suc` -| Lsuc+ , +𝕄 p;
    I2 <- `[ m ; j col ∈ 𝕄 ] ⟹ (m suc) + (j suc) = (m + j suc) suc` -| Lsuc+ , +𝕄 , 𝕄0s p;
    R2 <- `[ m ; j col ∈ 𝕄 ] ⟹ |s ap ((m + j suc) suc) ap ((m suc) suc) = |s ap ((m + j suc) suc) ap (m suc) + (((m + j suc) suc) choose (m suc)) ⋅ (|a ↑ { m suc } ⋅ |b ↑ { j suc } )` -| hyR , I2 , 𝕄0s v;
    R3 <- `[ m ; j col ∈ 𝕄 ] ⟹ |s ap (m + j suc) ap ((m suc) suc) = |s ap (m + j suc) ap (m suc) + ((m + j suc) choose (m suc)) ⋅ (|a ↑ { m suc } ⋅ |b ↑ j)` -| hyR , I1 , 𝕄0s v;
    R4 <- `[ m ; j col ∈ 𝕄 ] ⟹ |s ap (m + j suc) ap (m suc) = |s ap (m + j suc) ap (m) + ((m + j suc) choose m) ⋅ (|a ↑ m ⋅ |b ↑ { j suc } )` -| hyR , 𝕄0s v;
    Pa <- `m ∈ 𝕄 ⟹ |a ↑ { m suc } = |a ↑ m ⋅ |a` -| ↑𝕄 , hy1 p;
    Pb <- `j ∈ 𝕄 ⟹ |b ↑ { j suc } = |b ↑ j ⋅ |b` -| ↑𝕄 , hy1 p;
    Ks1 <- `[ m ; j col ∈ 𝕄 ] and |s ap ((m + j suc) suc) ap (m suc) = |b ⋅ |s ap (m + j suc) ap (m suc) + |a ⋅ |s ap (m + j suc) ap (m) ⟹ |s ap ((m + j suc) suc) ap ((m suc) suc) = |b ⋅ |s ap (m + j suc) ap ((m suc) suc) + |a ⋅ |s ap (m + j suc) ap (m suc)` -| R2 , R3 , R4 , choose𝕄 , Pa , Pb , A1 , LS∈ , LT∈ , choose∈𝕄 , ↑∈𝕄 , +∈𝕄 , hy1 , 𝕄0s v;
    Ks <- `m ∈ 𝕄 and [ ∀ j ∈ 𝕄 . |s ap ((m + j) suc) ap (m suc) = |b ⋅ |s ap (m + j) ap (m suc) + |a ⋅ |s ap (m + j) ap (m) ] ⟹ [ ∀ j ∈ 𝕄 . |s ap (((m suc) + j) suc) ap ((m suc) suc) = |b ⋅ |s ap ((m suc) + j) ap ((m suc) suc) + |a ⋅ |s ap ((m suc) + j) ap (m suc) ]` -| Ks1 , I1 , 𝕄0s v;
    LK <- `[ m ; j col ∈ 𝕄 ] ⟹ |s ap ((m + j) suc) ap (m suc) = |b ⋅ |s ap (m + j) ap (m suc) + |a ⋅ |s ap (m + j) ap (m)` -| IND𝕄[C_:=`\{ cls m | [ ∀ j ∈ 𝕄 . |s ap ((m + j) suc) ap (m suc) = |b ⋅ |s ap (m + j) ap (m suc) + |a ⋅ |s ap (m + j) ap (m) ] \}`] , Kb , Ks , 𝕄0s v;
    Mb <- `(|a + |b) ↑ 0 = |s ap (0) ap (0 suc)` -| hyR , hy0 , hy1 , choose𝕄 , ↑𝕄 , +𝕄 , L0+ , L⋅1 , +∈𝕄 , 𝕄0s , `1 ∈ 𝕄` v;
    M1 <- `n ∈ 𝕄 ⟹ |s ap (n) ap (n suc) = |s ap (n) ap (n) + |a ↑ n` -| hyR , Lnn , ↑𝕄 , +𝕄 , L⋅1 , ⋅C , ↑∈𝕄 , hy1 , 𝕄0s , `1 ∈ 𝕄` v;
    M2 <- `n ∈ 𝕄 ⟹ |s ap (n suc) ap ((n suc) suc) = |s ap (n suc) ap (n suc) + |a ↑ { n suc }` -| M1 , 𝕄0s v;
    M3 <- `n ∈ 𝕄 ⟹ |s ap (n suc) ap (n suc) = |b ⋅ |s ap (n) ap (n suc) + |a ⋅ |s ap (n) ap (n)` -| LK , +𝕄 , 𝕄0s v;
    A2 <- `[ x ; y ; a ; b ; p col ∈ 𝕄 ] and x = y + p ⟹ x ⋅ (a + b) = (b ⋅ x + a ⋅ y) + p ⋅ a` -| Ldist , Rdist , ⋅C , +A , +C , ⋅∈𝕄 , +∈𝕄 v;
    LSn <- `n ∈ 𝕄 ⟹ |s ap (n) ap (n) ∈ 𝕄 and |s ap (n) ap (n suc) ∈ 𝕄` -| LS∈ , M1 , +𝕄 , ↑∈𝕄 , +∈𝕄 , hy1 , 𝕄0s v;
    M4 <- `n ∈ 𝕄 ⟹ |s ap (n) ap (n suc) ⋅ (|a + |b) = |s ap (n suc) ap ((n suc) suc)` -| A2 , M1 , M2 , M3 , ↑𝕄 , LSn , ↑∈𝕄 , hy1 v;
    Ms <- `n ∈ 𝕄 and (|a + |b) ↑ n = |s ap (n) ap (n suc) ⟹ (|a + |b) ↑ { n suc } = |s ap (n suc) ap ((n suc) suc)` -| ↑𝕄 , M4 , +∈𝕄 , hy1 v;
    hyn <- `|n ∈ 𝕄` ;
    Lfix <- `(|a + |b) ↑ |n = |s ap (|n) ap (|n suc)` -| IND𝕄[C_:=`\{ cls n | (|a + |b) ↑ n = |s ap (n) ap (n suc) \}`] , Mb , Ms , hyn , 𝕄0s v;
    goal -| 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , ↑𝕄 , choose𝕄 , 1. h[fix];

articles3/44.book

`articles3/44.book`