Grace/Cumulus/Combinatorics/Binomial.g17

Open in Workbench Download source

Imports

Pigeonhole · NumberTheory.BinomialVanishing

Declarations

Source

1-- Identities for the binomial coefficient: Pascal's rule in additive form,2-- the first column, symmetry, positivity below the diagonal, absorption,3-- the factorial form with truncated subtraction, row sums adding up to a4-- power of two, and the hockey-stick identity5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Combinatorics.Binomial11import Pigeonhole12import NumberTheory.BinomialVanishing1314theorem natural.positive_of_nonzero (n : Nat)15  requires nonzero : n ≠ 016  shows 0 < n17proof18  have split := natural.zero_or_successor at n19  cases split with isZero | isSucc20  . exfalso21    exact nonzero with isZero22  . obtain ⟨k, kNat, shape⟩ := isSucc23    rw shape24    arith2526theorem natural.nonzero_of_positive (n : Nat)27  requires positive : 0 < n28  shows n ≠ 029proof30  intro zero31  rw zero at positive32  exact Less.irreflexive at 0 with positive3334theorem choose.natural (n k : Nat)35  shows Nat(n choose k)36proof37  typecheck3839-- Pascal's rule with successors written as additions.40theorem choose.pascal (n k : Nat)41  shows (n + 1) choose (k + 1) = (n choose k) + (n choose (k + 1))42proof43  have hn : n + 1 = succ(n) := add.right_one with *44  have hk : k + 1 = succ(k) := add.right_one with *45  rw [hn, hk]46  exact choose.succ_succ at n, k4748theorem choose.one_right (n : Nat)49  shows n choose 1 = n50proof51  induction n52  | zero => compute53  | k + 1 using ih =>54    have step := choose.pascal at k, 055    have one : 0 + 1 = 1 by compute56    rw one at step57    rw [step, choose.zero_right, ih]58    ring5960theorem choose.succ_self (n : Nat)61  shows (n + 1) choose n = n + 162proof63  induction n64  | zero => compute65  | k + 1 using ih =>66    have step := choose.pascal at k + 1, k67    rw [step, ih, choose.diagonal]68    rfl6970theorem choose.above_diagonal (n k : Nat)71  requires below : n < k72  shows n choose k = 073proof74  obtain ⟨d, dNat, shape⟩ := below75  have form : k = succ(n + d)76    rw ← shape77    ring78  rw form79  have le : n ≤ n + d by arith80  exact choose.vanishes at n, n + d with le8182theorem choose.eq_zero_iff (n k : Nat)83  shows n choose k = 0 ↔ n < k84proof85  constructor86  . intro zero87    by_contra notBelow88    have le := LessEqual.of_not_Less with notBelow89    obtain ⟨d, dNat, shape⟩ := le90    have form : n = d + k91      rw ← shape92      ring93    rw form at zero94    have row := choose.factorial at d95    have identity := row with k, assumption96    rw zero at identity97    have nonzero := factorial.nonzero at d + k98    apply nonzero99    rw ← identity100    ring101  . intro below102    exact choose.above_diagonal with below103104theorem choose.ne_zero_iff (n k : Nat)105  shows n choose k ≠ 0 ↔ k ≤ n106proof107  constructor108  . intro nonzero109    by_contra notLe110    have below := Less.of_not_LessEqual with notLe111    exact nonzero with (choose.above_diagonal with below)112  . intro le113    intro zero114    have iff := choose.eq_zero_iff at n, k115    have below := iff.forward with zero116    have strict := Less.transitive_LessEqual with below, le117    exact Less.irreflexive at n with strict118119theorem choose.positive (n k : Nat)120  requires le : k ≤ n121  shows 0 < n choose k122proof123  have iff := choose.ne_zero_iff at n, k124  have nonzero := iff.backward with le125  have chooseNat := choose.natural at n, k126  exact natural.positive_of_nonzero at n choose k with nonzero127128theorem choose.positive_iff (n k : Nat)129  shows 0 < n choose k ↔ k ≤ n130proof131  constructor132  . intro positive133    have iff := choose.ne_zero_iff at n, k134    have chooseNat := choose.natural at n, k135    have nonzero := natural.nonzero_of_positive at n choose k with positive136    exact iff.forward with nonzero137  . intro le138    exact choose.positive with le139140-- Symmetry of Pascal's triangle, in the form that needs no subtraction.141theorem choose.add_symmetric (m k : Nat)142  shows (m + k) choose k = (m + k) choose m143proof144  have rowM := choose.factorial at m145  have first := rowM with k, assumption146  have rowK := choose.factorial at k147  have second := rowK with m, assumption148  have commute : k + m = m + k by ring149  rw commute at second150  have factorialK := factorial.closed at k151  have factorialM := factorial.closed at m152  have swap : m! * k! = k! * m! by ring153  rw swap at second154  rw ← second at first155  have productNonzero := mul.nonzero with156    (factorial.nonzero at k), (factorial.nonzero at m)157  have leftNat := choose.natural at m + k, k158  have rightNat := choose.natural at m + k, m159  have balanced : (k! * m!) * ((m + k) choose k) = (k! * m!) * ((m + k) choose m) by ring [first]160  exact mul.left_cancel_positive with productNonzero, balanced161162theorem choose.symmetric (n k : Nat)163  requires le : k ≤ n164  shows n choose k = n choose (n - k)165proof166  obtain ⟨d, dNat, shape⟩ := le167  have form : n = d + k168    rw ← shape169    ring170  have difference : n - k = d171    rw form172    exact sub.add_right at d, k173  rw [difference, form]174  exact choose.add_symmetric at d, k175176theorem choose.sub_self (n : Nat)177  shows ∀ k, Nat(k) → k ≤ n → n choose (n - k) = n choose k178proof179  intros k kNat le180  symm181  exact choose.symmetric with le182183-- The factorial form n choose k · k! · (n − k)! = n!.184theorem choose.factorial_form (n k : Nat)185  requires le : k ≤ n186  shows (n choose k) * (k! * (n - k)!) = n!187proof188  obtain ⟨d, dNat, shape⟩ := le189  have form : n = d + k190    rw ← shape191    ring192  have difference : n - k = d193    rw form194    exact sub.add_right at d, k195  rw [difference, form]196  have row := choose.factorial at d197  exact row with k, assumption198199theorem choose.two (n : Nat)200  shows 2 * ((n + 1) choose 2) = (n + 1) * n201proof202  induction n203  | zero => compute204  | k + 1 using ih =>205    have step := choose.pascal at k + 1, 1206    have two : 1 + 1 = 2 by compute207    rw two at step208    rw [step, choose.one_right]209    have chooseNat := choose.natural at k + 1, 2210    ring [ih]211212theorem choose.two_sub (n : Nat)213  shows 2 * (n choose 2) = n * (n - 1)214proof215  have split := natural.zero_or_successor at n216  cases split with isZero | isSucc217  . rw isZero218    compute219  . obtain ⟨k, kNat, shape⟩ := isSucc220    have one : succ(k) = k + 1221      symm222      exact add.right_one at k223    rw [shape, one]224    have difference : k + 1 - 1 = k := sub.add_right at k, 1225    rw difference226    exact choose.two at k227228-- Absorption: (k + 1) · (n + 1 choose k + 1) = (n + 1) · (n choose k).229theorem choose.absorption (n : Nat)230  shows231    ∀ k, Nat(k) → (k + 1) * ((n + 1) choose (k + 1)) = (n + 1) * (n choose k)232proof233  induction n234  | zero =>235    intros k kNat236    have split := natural.zero_or_successor at k237    cases split with isZero | isSucc238    . rw isZero239      compute240    . obtain ⟨j, jNat, shape⟩ := isSucc241      rw shape242      have vanishTop : (0 + 1) choose (succ(j) + 1) = 0243        have le : 0 + 1 ≤ succ(j) by arith244        have hs : succ(j) + 1 = succ(succ(j)) := add.right_one with *245        rw hs246        exact choose.vanishes at 0 + 1, succ(j) with le247      have vanishBottom : 0 choose succ(j) = 0 := choose.zero_left at j248      rw [vanishTop, vanishBottom]249      ring250  | m + 1 using ih =>251    intros k kNat252    have split := natural.zero_or_successor at k253    cases split with isZero | isSucc254    . rw isZero255      have top := choose.pascal at m + 1, 0256      have one : 0 + 1 = 1 by compute257      rw one at top258      rw [one, top, choose.zero_right, choose.one_right]259      ring260    . obtain ⟨j, jNat, shape⟩ := isSucc261      have hj : succ(j) = j + 1262        symm263        exact add.right_one at j264      rw [shape, hj]265      have top := choose.pascal at m + 1, j + 1266      have first := ih with j, jNat267      have sjNat : Nat(j + 1) by typecheck268      have second := ih with j + 1, sjNat269      have inner := choose.pascal at m, j270      have aNat := choose.natural at m + 1, j + 1271      have bNat := choose.natural at m + 1, j + 1 + 1272      have pNat := choose.natural at m, j273      have qNat := choose.natural at m, j + 1274      rw top275      ring [second, first, inner]276277theorem choose.absorption_at (n k : Nat)278  shows (k + 1) * ((n + 1) choose (k + 1)) = (n + 1) * (n choose k)279proof280  have all := choose.absorption at n281  exact all with k, assumption282283-- Each row of Pascal's triangle is pointwise below the next.284theorem choose.monotone_row (n k : Nat)285  shows n choose k ≤ (n + 1) choose k286proof287  have split := natural.zero_or_successor at k288  cases split with isZero | isSucc289  . rw [isZero, choose.zero_right, choose.zero_right]290    exact LessEqual.reflexive at 1291  . obtain ⟨j, jNat, shape⟩ := isSucc292    have hj : succ(j) = j + 1293      symm294      exact add.right_one at j295    rw [shape, hj, choose.pascal]296    have leftNat := choose.natural at n, j297    have rightNat := choose.natural at n, j + 1298    arith299300-- Partial sums along a row of Pascal's triangle.301def chooseRowSum (n k : Nat) → Nat302  | n, zero => 0303  | n, succ(k) => chooseRowSum(n, k) + choose(n, k)304  descends k305306theorem chooseRowSum.zero (n : Nat)307  shows chooseRowSum(n, 0) = 0308proof309  simp [chooseRowSum]310311theorem chooseRowSum.succ (n k : Nat)312  shows chooseRowSum(n, k + 1) = chooseRowSum(n, k) + (n choose k)313proof314  have hk : k + 1 = succ(k) := add.right_one with *315  rw hk316  simp [chooseRowSum]317318theorem chooseRowSum.natural (n k : Nat)319  shows Nat(chooseRowSum(n, k))320proof321  induction k322  | zero =>323    rw chooseRowSum.zero324    typecheck325  | j + 1 using ih =>326    rw chooseRowSum.succ327    have chooseNat := choose.natural at n, j328    typecheck329330theorem chooseRowSum.one (n : Nat)331  shows chooseRowSum(n, 1) = 1332proof333  simp [chooseRowSum, choose.zero_right]334335theorem chooseRowSum.pascal (n k : Nat)336  shows chooseRowSum(n + 1, k + 1) = chooseRowSum(n, k) + chooseRowSum(n, k + 1)337proof338  induction k339  | zero =>340    have one : 0 + 1 = 1 by compute341    rw [one, chooseRowSum.one, chooseRowSum.zero, chooseRowSum.one]342    compute343  | j + 1 using ih =>344    have top := chooseRowSum.succ at n + 1, j + 1345    have pascalRule := choose.pascal at n, j346    have right := chooseRowSum.succ at n, j + 1347    have left := chooseRowSum.succ at n, j348    have sumNat := chooseRowSum.natural at n, j349    have sumNat1 := chooseRowSum.natural at n, j + 1350    have cNat := choose.natural at n, j351    have cNat1 := choose.natural at n, j + 1352    rw [top, ih, pascalRule, right]353    ring [left]354355theorem chooseRowSum.monotone (n k d : Nat)356  shows chooseRowSum(n, k) ≤ chooseRowSum(n, k + d)357proof358  induction d359  | zero =>360    have shape : k + 0 = k by ring361    rw shape362    have sumNat := chooseRowSum.natural at n, k363    exact LessEqual.reflexive at chooseRowSum(n, k)364  | j + 1 using ih =>365    have shape : k + (j + 1) = (k + j) + 1 by ring366    rw [shape, chooseRowSum.succ]367    have sumNat := chooseRowSum.natural at n, k368    have sumNatJ := chooseRowSum.natural at n, k + j369    have cNat := choose.natural at n, k + j370    arith371372theorem chooseRowSum.term_le (n k m : Nat)373  requires below : k < m374  shows n choose k ≤ chooseRowSum(n, m)375proof376  induction m377  | zero =>378    intro below379    have cNat := choose.natural at n, k380    arith381  | j + 1 using ih =>382    intro below383    rw chooseRowSum.succ384    have sumNat := chooseRowSum.natural at n, j385    have cNat := choose.natural at n, k386    have cNatJ := choose.natural at n, j387    have alternatives : k = j ∨ k ≠ j by tauto388    cases alternatives with same | different389    . rw same390      arith391    . have hj : j + 1 = succ(j) := add.right_one with *392      rw hj at below393      have strict := Less.of_successor_upper_ne with below, different394      have bound := ih with strict395      arith396397-- The row sums: the full row adds up to 2 ^ n.398theorem chooseRowSum.full (n : Nat)399  shows chooseRowSum(n, n + 1) = 2 ^ n400proof401  induction n402  | zero =>403    have one : 0 + 1 = 1 by compute404    rw [one, chooseRowSum.one, pow.zero]405    rfl406  | k + 1 using ih =>407    rw chooseRowSum.pascal408    have expand := chooseRowSum.succ at k, k + 1409    rw [expand, ih]410    have below : k < k + 1 by arith411    have vanish := choose.above_diagonal with below412    rw vanish413    have hs : k + 1 = succ(k) := add.right_one with *414    rw [hs, pow.succ]415    have powNat := pow.closed at 2, k416    ring417418theorem chooseRowSum.beyond (n d : Nat)419  shows chooseRowSum(n, n + 1 + d) = 2 ^ n420proof421  induction d422  | zero =>423    have shape : n + 1 + 0 = n + 1 by ring424    rw shape425    exact chooseRowSum.full at n426  | j + 1 using ih =>427    have shape : n + 1 + (j + 1) = (n + 1 + j) + 1 by ring428    rw [shape, chooseRowSum.succ, ih]429    have below : n < n + 1 + j by arith430    have vanish := choose.above_diagonal with below431    rw vanish432    have powNat := pow.closed at 2, n433    ring434435theorem choose.le_pow (n k : Nat)436  shows n choose k ≤ 2 ^ n437proof438  have powNat := pow.closed at 2, n439  have cNat := choose.natural at n, k440  have alternatives := LessEqual.total at k, n441  cases alternatives with le | ge442  . have below : k < n + 1 by arith443    have bound := chooseRowSum.term_le at n, k, n + 1 with below444    rw chooseRowSum.full at bound445    exact bound446  . have split : k = n ∨ k ≠ n by tauto447    cases split with same | different448    . rw same449      have below : n < n + 1 by arith450      have bound := chooseRowSum.term_le at n, n, n + 1 with below451      rw chooseRowSum.full at bound452      exact bound453    . have strict : n < k454        obtain ⟨d, dNat, shape⟩ := ge455        have dSplit := natural.zero_or_successor at d456        cases dSplit with dZero | dSucc457        . exfalso458          apply different459          rw [dZero] at shape460          rw ← shape461          ring462        . obtain ⟨e, eNat, dShape⟩ := dSucc463          rw dShape at shape464          rw ← shape465          arith466      have vanish := choose.above_diagonal with strict467      rw vanish468      arith469470-- Partial sums down a diagonal of Pascal's triangle.471def diagonalSum (k m : Nat) → Nat472  | k, zero => 0473  | k, succ(m) => diagonalSum(k, m) + choose(m + k, k)474  descends m475476theorem diagonalSum.zero (k : Nat)477  shows diagonalSum(k, 0) = 0478proof479  simp [diagonalSum]480481theorem diagonalSum.succ (k m : Nat)482  shows diagonalSum(k, m + 1) = diagonalSum(k, m) + ((m + k) choose k)483proof484  have hm : m + 1 = succ(m) := add.right_one with *485  rw hm486  simp [diagonalSum]487488theorem diagonalSum.natural (k m : Nat)489  shows Nat(diagonalSum(k, m))490proof491  induction m492  | zero =>493    rw diagonalSum.zero494    typecheck495  | j + 1 using ih =>496    rw diagonalSum.succ497    have cNat := choose.natural at j + k, k498    typecheck499500-- The hockey-stick identity.501theorem diagonalSum.hockey_stick (k m : Nat)502  shows diagonalSum(k, m) = (m + k) choose (k + 1)503proof504  induction m505  | zero =>506    have shape : 0 + k = k by ring507    rw [diagonalSum.zero, shape]508    have below : k < k + 1 by arith509    symm510    exact choose.above_diagonal with below511  | j + 1 using ih =>512    rw [diagonalSum.succ, ih]513    have shape : j + 1 + k = (j + k) + 1 by ring514    rw [shape, choose.pascal]515    have leftNat := choose.natural at j + k, k516    have rightNat := choose.natural at j + k, k + 1517    ring518519theorem factorial.one520  shows 1! = 1521proof522  compute523524theorem factorial.two525  shows 2! = 2526proof527  compute528529theorem factorial.positive (n : Nat)530  shows 0 < n!531proof532  have nonzero := factorial.nonzero at n533  have closed := factorial.closed at n534  exact natural.positive_of_nonzero at n! with nonzero535536theorem factorial.ge_one (n : Nat)537  shows 1 ≤ n!538proof539  have positive := factorial.positive at n540  have closed := factorial.closed at n541  arith542543theorem factorial.monotone (n : Nat)544  shows n! ≤ (n + 1)!545proof546  rw factorial.succ547  have closed := factorial.closed at n548  have expand : (n + 1) * n! = n * n! + n! by ring549  rw expand550  have productNat : Nat(n * n!) by typecheck551  arith552553theorem factorial.le_of_le (m d : Nat)554  shows m! ≤ (m + d)!555proof556  induction d557  | zero =>558    have shape : m + 0 = m by ring559    rw shape560    have closed := factorial.closed at m561    exact LessEqual.reflexive at m!562  | j + 1 using ih =>563    have shape : m + (j + 1) = (m + j) + 1 by ring564    rw shape565    have step := factorial.monotone at m + j566    have closedM := factorial.closed at m567    have closedJ := factorial.closed at m + j568    have closedTop := factorial.closed at m + j + 1569    exact LessEqual.transitive with ih, step570