Grace/Cumulus/Combinatorics/BinomialMore.g17

Open in Workbench Download source

Imports

Derangements

Declarations

Source

1-- Further identities for the binomial coefficient: the weighted row sum2-- ∑ k · (n choose k) = n · 2 ^ (n − 1), the even-index and odd-index row3-- sums agreeing at 2 ^ (n − 1), the ratio of neighbouring entries in4-- product form, unimodality of a row, and the third column5-- 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.BinomialMore11import Derangements1213-- Partial sums ∑_{i < k} i · (n choose i).14def weightedRowSum (n k : Nat) → Nat15  | n, zero => 016  | n, succ(k) => weightedRowSum(n, k) + k * choose(n, k)17  descends k1819theorem weightedRowSum.zero (n : Nat)20  shows weightedRowSum(n, 0) = 021proof22  simp [weightedRowSum]2324theorem weightedRowSum.succ (n k : Nat)25  shows weightedRowSum(n, k + 1) = weightedRowSum(n, k) + k * (n choose k)26proof27  have hk : k + 1 = succ(k) := add.right_one with *28  rw hk29  simp [weightedRowSum]3031theorem weightedRowSum.natural (n k : Nat)32  shows Nat(weightedRowSum(n, k))33proof34  induction k35  | zero =>36    rw weightedRowSum.zero37    typecheck38  | j + 1 using ih =>39    rw weightedRowSum.succ40    have cNat := choose.natural at n, j41    typecheck4243theorem weightedRowSum.one (n : Nat)44  shows weightedRowSum(n, 1) = 045proof46  have one : 0 + 1 = 1 by compute47  rw ← one48  rw [weightedRowSum.succ, weightedRowSum.zero, choose.zero_right]49  compute5051-- Absorption termwise:52-- ∑_{i ≤ k} i · (n + 1 choose i) = (n + 1) · ∑_{i < k} (n choose i).53theorem weightedRowSum.shift (n k : Nat)54  shows weightedRowSum(n + 1, k + 1) = (n + 1) * chooseRowSum(n, k)55proof56  induction k57  | zero =>58    have one : 0 + 1 = 1 by compute59    rw [one, weightedRowSum.one, chooseRowSum.zero]60    ring61  | j + 1 using ih =>62    rw [weightedRowSum.succ, ih, chooseRowSum.succ]63    have absorb := choose.absorption_at at n, j64    have rowNat := chooseRowSum.natural at n, j65    have cNat := choose.natural at n, j66    have topNat := choose.natural at n + 1, j + 167    ring [absorb]6869-- ∑_{k ≤ n + 1} k · (n + 1 choose k) = (n + 1) · 2 ^ n.70theorem weightedRowSum.full (n : Nat)71  shows weightedRowSum(n + 1, n + 2) = (n + 1) * 2 ^ n72proof73  have shape : n + 2 = (n + 1) + 1 by ring74  rw [shape, weightedRowSum.shift, chooseRowSum.full]75  rfl7677theorem weightedRowSum.double (n : Nat)78  shows 2 * weightedRowSum(n, n + 1) = n * 2 ^ n79proof80  have split := natural.zero_or_successor at n81  cases split with isZero | isSucc82  . rw isZero83    compute84  . obtain ⟨j, jNat, shape⟩ := isSucc85    have hj : succ(j) = j + 186      symm87      exact add.right_one at j88    have two : j + 1 + 1 = j + 2 by ring89    rw [shape, hj, two, weightedRowSum.full, pow.add_one]90    have powNat := pow.closed at 2, j91    ring9293-- Partial sums over the even and the odd columns of a row.94def evenRowSum (n k : Nat) → Nat95  | n, zero => 096  | n, succ(k) => evenRowSum(n, k) + choose(n, 2 * k)97  descends k9899def oddRowSum (n k : Nat) → Nat100  | n, zero => 0101  | n, succ(k) => oddRowSum(n, k) + choose(n, 2 * k + 1)102  descends k103104theorem evenRowSum.zero (n : Nat)105  shows evenRowSum(n, 0) = 0106proof107  simp [evenRowSum]108109theorem evenRowSum.succ (n k : Nat)110  shows evenRowSum(n, k + 1) = evenRowSum(n, k) + (n choose (2 * k))111proof112  have hk : k + 1 = succ(k) := add.right_one with *113  rw hk114  simp [evenRowSum]115116theorem evenRowSum.natural (n k : Nat)117  shows Nat(evenRowSum(n, k))118proof119  induction k120  | zero =>121    rw evenRowSum.zero122    typecheck123  | j + 1 using ih =>124    rw evenRowSum.succ125    have cNat := choose.natural at n, 2 * j126    typecheck127128theorem oddRowSum.zero (n : Nat)129  shows oddRowSum(n, 0) = 0130proof131  simp [oddRowSum]132133theorem oddRowSum.succ (n k : Nat)134  shows oddRowSum(n, k + 1) = oddRowSum(n, k) + (n choose (2 * k + 1))135proof136  have hk : k + 1 = succ(k) := add.right_one with *137  rw hk138  simp [oddRowSum]139140theorem oddRowSum.natural (n k : Nat)141  shows Nat(oddRowSum(n, k))142proof143  induction k144  | zero =>145    rw oddRowSum.zero146    typecheck147  | j + 1 using ih =>148    rw oddRowSum.succ149    have cNat := choose.natural at n, 2 * j + 1150    typecheck151152theorem evenRowSum.one (n : Nat)153  shows evenRowSum(n, 1) = 1154proof155  have one : 0 + 1 = 1 by compute156  rw ← one157  rw [evenRowSum.succ, evenRowSum.zero]158  have twice : 2 * 0 = 0 by compute159  rw [twice, choose.zero_right]160  compute161162theorem oddRowSum.one (n : Nat)163  shows oddRowSum(n, 1) = n164proof165  have one : 0 + 1 = 1 by compute166  rw ← one167  rw [oddRowSum.succ, oddRowSum.zero]168  have twice : 2 * 0 = 0 by compute169  rw [twice, one, choose.one_right]170  ring171172-- Pascal's rule column by column: the even sums of row n + 1 come from the173-- even and the odd sums of row n.174theorem evenRowSum.pascal (n k : Nat)175  shows evenRowSum(n + 1, k + 1) = evenRowSum(n, k + 1) + oddRowSum(n, k)176proof177  induction k178  | zero =>179    have one : 0 + 1 = 1 by compute180    rw [one, evenRowSum.one, evenRowSum.one, oddRowSum.zero]181    compute182  | j + 1 using ih =>183    have top := evenRowSum.succ at n + 1, j + 1184    have right := evenRowSum.succ at n, j + 1185    have low := oddRowSum.succ at n, j186    rw [top, ih, right, low]187    have shape : 2 * (j + 1) = 2 * j + 1 + 1 by ring188    rw [shape, choose.pascal]189    have aNat := evenRowSum.natural at n, j + 1190    have bNat := oddRowSum.natural at n, j191    have cNat := choose.natural at n, 2 * j + 1192    have dNat := choose.natural at n, 2 * j + 1 + 1193    ring194195theorem oddRowSum.pascal (n k : Nat)196  shows oddRowSum(n + 1, k) = evenRowSum(n, k) + oddRowSum(n, k)197proof198  induction k199  | zero =>200    rw [oddRowSum.zero, evenRowSum.zero, oddRowSum.zero]201    compute202  | j + 1 using ih =>203    rw [oddRowSum.succ, ih, evenRowSum.succ, oddRowSum.succ, choose.pascal]204    have aNat := evenRowSum.natural at n, j205    have bNat := oddRowSum.natural at n, j206    have cNat := choose.natural at n, 2 * j207    have dNat := choose.natural at n, 2 * j + 1208    ring209210-- A row sum up to an even bound splits into its even and odd parts.211theorem chooseRowSum.split_parity (n k : Nat)212  shows chooseRowSum(n, 2 * k) = evenRowSum(n, k) + oddRowSum(n, k)213proof214  induction k215  | zero =>216    have twice : 2 * 0 = 0 by compute217    rw [twice, chooseRowSum.zero, evenRowSum.zero, oddRowSum.zero]218    compute219  | j + 1 using ih =>220    have shape : 2 * (j + 1) = (2 * j + 1) + 1 by ring221    rw [shape, chooseRowSum.succ, chooseRowSum.succ, ih]222    rw [evenRowSum.succ, oddRowSum.succ]223    have aNat := evenRowSum.natural at n, j224    have bNat := oddRowSum.natural at n, j225    have cNat := choose.natural at n, 2 * j226    have dNat := choose.natural at n, 2 * j + 1227    ring228229theorem evenRowSum.add_odd (n : Nat)230  shows evenRowSum(n, n + 1) + oddRowSum(n, n + 1) = 2 ^ n231proof232  rw ← chooseRowSum.split_parity233  have shape : 2 * (n + 1) = n + 1 + (n + 1) by ring234  rw shape235  exact chooseRowSum.beyond at n, n + 1236237theorem evenRowSum.beyond (n d : Nat)238  shows evenRowSum(n, n + 1 + d) = evenRowSum(n, n + 1)239proof240  induction d241  | zero =>242    have shape : n + 1 + 0 = n + 1 by ring243    rw shape244    rfl245  | j + 1 using ih =>246    have shape : n + 1 + (j + 1) = (n + 1 + j) + 1 by ring247    rw [shape, evenRowSum.succ, ih]248    have below : n < 2 * (n + 1 + j) by arith249    have vanish := choose.above_diagonal with below250    rw vanish251    have sumNat := evenRowSum.natural at n, n + 1252    ring253254theorem oddRowSum.beyond (n d : Nat)255  shows oddRowSum(n, n + 1 + d) = oddRowSum(n, n + 1)256proof257  induction d258  | zero =>259    have shape : n + 1 + 0 = n + 1 by ring260    rw shape261    rfl262  | j + 1 using ih =>263    have shape : n + 1 + (j + 1) = (n + 1 + j) + 1 by ring264    rw [shape, oddRowSum.succ, ih]265    have below : n < 2 * (n + 1 + j) + 1 by arith266    have vanish := choose.above_diagonal with below267    rw vanish268    have sumNat := oddRowSum.natural at n, n + 1269    ring270271-- The even columns of row n + 1 add up to 2 ^ n, and so do the odd columns.272theorem evenRowSum.full (n : Nat)273  shows evenRowSum(n + 1, n + 2) = 2 ^ n274proof275  have shape : n + 2 = (n + 1) + 1 by ring276  rw [shape, evenRowSum.pascal]277  have tail := evenRowSum.beyond at n, 1278  rw tail279  exact evenRowSum.add_odd at n280281theorem oddRowSum.full (n : Nat)282  shows oddRowSum(n + 1, n + 2) = 2 ^ n283proof284  rw oddRowSum.pascal285  have shape : n + 2 = n + 1 + 1 by ring286  rw shape287  have evenTail := evenRowSum.beyond at n, 1288  have oddTail := oddRowSum.beyond at n, 1289  rw [evenTail, oddTail]290  exact evenRowSum.add_odd at n291292-- The alternating row sum vanishes: even and odd columns balance.293theorem choose.alternating (n : Nat)294  shows evenRowSum(n + 1, n + 2) = oddRowSum(n + 1, n + 2)295proof296  rw [evenRowSum.full, oddRowSum.full]297  rfl298299-- The complementary absorption law300-- (m − k + 1) · (m + 1 choose k) = (m + 1) · (m choose k).301theorem choose.absorption_complement (m k : Nat)302  requires le : k ≤ m303  shows (m - k + 1) * ((m + 1) choose k) = (m + 1) * (m choose k)304proof305  obtain ⟨d, dNat, shape⟩ := le306  have difference : m - k = d307    rw ← shape308    exact sub.add_left at d, k309  rw [difference, ← shape]310  have first := choose.add_symmetric at d + 1, k311  have shapeA : k + d + 1 = d + 1 + k by ring312  rw [shapeA, first]313  have second := choose.add_symmetric at d, k314  have shapeB : k + d = d + k by ring315  rw [shapeB, second]316  have absorb := choose.absorption_at at d + k, d317  have aNat := choose.natural at d + 1 + k, d + 1318  have bNat := choose.natural at d + k, d319  ring [absorb]320321-- Neighbouring entries of a row:322-- (k + 1) · (m + 1 choose k + 1) = (m − k + 1) · (m + 1 choose k).323theorem choose.ratio (m k : Nat)324  requires le : k ≤ m325  shows (k + 1) * ((m + 1) choose (k + 1)) = (m - k + 1) * ((m + 1) choose k)326proof327  have complement := choose.absorption_complement with le328  rw [choose.absorption_at, complement]329  rfl330331theorem choose.le_succ_of_below_half (m k : Nat)332  requires half : 2 * k ≤ m333  shows (m + 1) choose k ≤ (m + 1) choose (k + 1)334proof335  have le : k ≤ m by arith336  have ratio := choose.ratio with le337  have subNat := sub.closed at m, k338  have cancel := sub.add_cancel_left with le339  have coefficient : k + 1 ≤ m - k + 1 by arith340  have aNat := choose.natural at m + 1, k341  have bNat := choose.natural at m + 1, k + 1342  have scaled := LessEqual.mul_right at k + 1, m - k + 1, (m + 1) choose k343    with coefficient344  rw ← ratio at scaled345  have positive : 0 < k + 1 by arith346  have nonzero := Less.ne_zero_of_positive with positive347  exact LessEqual.mul_left_cancel_positive with nonzero, scaled348349theorem choose.lt_succ_of_below_half (m k : Nat)350  requires half : 2 * k + 1 ≤ m351  shows (m + 1) choose k < (m + 1) choose (k + 1)352proof353  have le : k ≤ m by arith354  have ratio := choose.ratio with le355  have subNat := sub.closed at m, k356  have cancel := sub.add_cancel_left with le357  have coefficient : k + 1 < m - k + 1 by arith358  have aNat := choose.natural at m + 1, k359  have bNat := choose.natural at m + 1, k + 1360  have leTop : k ≤ m + 1 by arith361  have positive := choose.positive with leTop362  have nonzero := Less.ne_zero_of_positive with positive363  have scaled := Less.mul_right at k + 1, m - k + 1, (m + 1) choose k364    with nonzero, coefficient365  rw ← ratio at scaled366  have gapPositive : 0 < k + 1 by arith367  have gap := Less.ne_zero_of_positive with gapPositive368  exact Less.mul_left_cancel_positive with gap, scaled369370-- A row of Pascal's triangle increases up to its middle.371theorem choose.monotone_to_half (n j d : Nat)372  requires half : 2 * (j + d) ≤ n373  shows n choose j ≤ n choose (j + d)374proof375  induction d376  | zero =>377    intro half378    have shape : j + 0 = j by ring379    rw shape380    have cNat := choose.natural at n, j381    exact LessEqual.reflexive at n choose j382  | k + 1 using ih =>383    intro half384    have earlier : 2 * (j + k) ≤ n by arith385    have inner := ih with earlier386    have positive : 0 < n by arith387    obtain ⟨m, mNat, shape⟩ := Less.exists_add_one with positive388    have form : n = m + 1389      rw shape390      ring391    rw form at inner392    rw form at half393    rw form394    have below : 2 * (j + k) ≤ m by arith395    have step := choose.le_succ_of_below_half at m, j + k with below396    have shapeD : j + (k + 1) = j + k + 1 by ring397    rw shapeD398    have aNat := choose.natural at m + 1, j399    have bNat := choose.natural at m + 1, j + k400    have cNat := choose.natural at m + 1, j + k + 1401    exact LessEqual.transitive with inner, step402403theorem choose.central_dominates_below (n k : Nat)404  requires le : k ≤ n405  shows (2 * n) choose k ≤ (2 * n) choose n406proof407  obtain ⟨d, dNat, shape⟩ := le408  have half : 2 * (k + d) ≤ 2 * n409    rw shape410    have doubleNat : Nat(2 * n) by typecheck411    exact LessEqual.reflexive at 2 * n412  have bound := choose.monotone_to_half at 2 * n, k, d with half413  rw shape at bound414  exact bound415416-- The central entry dominates every entry of an even row.417theorem choose.le_central (n k : Nat)418  shows (2 * n) choose k ≤ (2 * n) choose n419proof420  have alternatives := Less.or_LessEqual at n, k421  cases alternatives with above | le422  . have split := Less.or_LessEqual at 2 * n, k423    cases split with far | inRow424    . have vanish := choose.above_diagonal with far425      rw vanish426      have cNat := choose.natural at 2 * n, n427      arith428    . have mirror := choose.symmetric at 2 * n, k with inRow429      rw mirror430      have subNat := sub.closed at 2 * n, k431      have iff := sub.le_iff at 2 * n, k, n432      have small : 2 * n ≤ k + n by arith433      have le := iff.backward with small434      exact choose.central_dominates_below with le435  . exact choose.central_dominates_below with le436437theorem choose.odd_dominates_below (n k : Nat)438  requires le : k ≤ n439  shows (2 * n + 1) choose k ≤ (2 * n + 1) choose n440proof441  obtain ⟨d, dNat, shape⟩ := le442  have half : 2 * (k + d) ≤ 2 * n + 1443    rw shape444    arith445  have bound := choose.monotone_to_half at 2 * n + 1, k, d with half446  rw shape at bound447  exact bound448449-- The two middle entries dominate every entry of an odd row.450theorem choose.le_central_odd (n k : Nat)451  shows (2 * n + 1) choose k ≤ (2 * n + 1) choose n452proof453  have alternatives := Less.or_LessEqual at n, k454  cases alternatives with above | le455  . have split := Less.or_LessEqual at 2 * n + 1, k456    cases split with far | inRow457    . have vanish := choose.above_diagonal with far458      rw vanish459      have cNat := choose.natural at 2 * n + 1, n460      arith461    . have mirror := choose.symmetric at 2 * n + 1, k with inRow462      rw mirror463      have subNat := sub.closed at 2 * n + 1, k464      have iff := sub.le_iff at 2 * n + 1, k, n465      have small : 2 * n + 1 ≤ k + n by arith466      have le := iff.backward with small467      exact choose.odd_dominates_below with le468  . exact choose.odd_dominates_below with le469470theorem choose.pascal_le_left (n k : Nat)471  shows n choose k ≤ (n + 1) choose (k + 1)472proof473  rw choose.pascal474  have aNat := choose.natural at n, k475  have bNat := choose.natural at n, k + 1476  arith477478theorem choose.pascal_le_right (n k : Nat)479  shows n choose (k + 1) ≤ (n + 1) choose (k + 1)480proof481  rw choose.pascal482  have aNat := choose.natural at n, k483  have bNat := choose.natural at n, k + 1484  arith485486-- The third column: 6 · (n + 3 choose 3) = (n + 3)(n + 2)(n + 1).487theorem choose.three (n : Nat)488  shows 6 * ((n + 3) choose 3) = (n + 3) * (n + 2) * (n + 1)489proof490  have absorb := choose.absorption_at at n + 2, 2491  have three : 2 + 1 = 3 by compute492  have shape : n + 2 + 1 = n + 3 by ring493  rw [three, shape] at absorb494  have second := choose.two at n + 1495  have shape2 : n + 1 + 1 = n + 2 by ring496  rw shape2 at second497  have aNat := choose.natural at n + 3, 3498  have bNat := choose.natural at n + 2, 2499  ring [absorb, second]500