Grace/Cumulus/Combinatorics/Vandermonde.g17

Open in Workbench Download source

Imports

Lucas · Nat.SubtractionLemmas

Declarations

Source

1-- Vandermonde's identity: the convolution of two rows of Pascal's triangle2-- is an entry of a later row, the sum of the squares of a row is the central3-- binomial coefficient, and the bounds that follow from it4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Combinatorics.Vandermonde10import Lucas11import Nat.SubtractionLemmas1213-- The partial convolution ∑_{i < k} (m choose i) · (n choose (r − i)).14def chooseConvolution (m n r k : Nat) → Nat15  | m, n, r, zero => 016  | m, n, r, succ(k) =>17    chooseConvolution(m, n, r, k) + choose(m, k) * choose(n, sub(r, k))18  descends k1920theorem chooseConvolution.zero (m n r : Nat)21  shows chooseConvolution(m, n, r, 0) = 022proof23  simp [chooseConvolution]2425theorem chooseConvolution.succ (m n r k : Nat)26  shows chooseConvolution(m, n, r, k + 1) =27    chooseConvolution(m, n, r, k) + (m choose k) * (n choose (r - k))28proof29  have hk : k + 1 = succ(k) := add.right_one with *30  rw hk31  simp [chooseConvolution]3233theorem chooseConvolution.natural (m n r k : Nat)34  shows Nat(chooseConvolution(m, n, r, k))35proof36  induction k37  | zero =>38    rw chooseConvolution.zero39    typecheck40  | j + 1 using ih =>41    rw chooseConvolution.succ42    have leftNat := choose.natural at m, j43    have subNat := sub.closed at r, j44    have rightNat := choose.natural at n, r - j45    typecheck4647theorem chooseConvolution.one (m n r : Nat)48  shows chooseConvolution(m, n, r, 1) = n choose r49proof50  have one : 0 + 1 = 1 by compute51  rw ← one52  rw [chooseConvolution.succ, chooseConvolution.zero, choose.zero_right]53  rw sub.zero_right54  have cNat := choose.natural at n, r55  ring5657-- Row 0 of the triangle contributes only its first entry.58theorem chooseConvolution.zero_left (n r k : Nat)59  shows chooseConvolution(0, n, r, k + 1) = n choose r60proof61  induction k62  | zero =>63    have one : 0 + 1 = 1 by compute64    rw one65    exact chooseConvolution.one at 0, n, r66  | j + 1 using ih =>67    rw [chooseConvolution.succ, ih]68    have hj : j + 1 = succ(j) := add.right_one with *69    rw [hj, choose.zero_left]70    have cNat := choose.natural at n, r71    have subNat := sub.closed at r, succ(j)72    have rightNat := choose.natural at n, r - succ(j)73    ring7475-- Pascal's rule for the convolution: the first row advances by one when the76-- target splits into the sums for r + 1 and for r.77theorem chooseConvolution.pascal (m n r k : Nat)78  shows chooseConvolution(m + 1, n, r + 1, k + 1) =79    chooseConvolution(m, n, r + 1, k + 1) + chooseConvolution(m, n, r, k)80proof81  induction k82  | zero =>83    have one : 0 + 1 = 1 by compute84    rw [one, chooseConvolution.one, chooseConvolution.one]85    rw chooseConvolution.zero86    have cNat := choose.natural at n, r + 187    ring88  | j + 1 using ih =>89    have top := chooseConvolution.succ at m + 1, n, r + 1, j + 190    have middle := chooseConvolution.succ at m, n, r + 1, j + 191    have low := chooseConvolution.succ at m, n, r, j92    have pascalRule := choose.pascal at m, j93    have shift : r + 1 - (j + 1) = r - j := sub.add_one_both at r, j94    rw [top, ih, middle, low, pascalRule, shift]95    have aNat := chooseConvolution.natural at m, n, r + 1, j + 196    have bNat := chooseConvolution.natural at m, n, r, j97    have cNat := choose.natural at m, j98    have dNat := choose.natural at m, j + 199    have subNat := sub.closed at r, j100    have eNat := choose.natural at n, r - j101    ring102103-- Vandermonde's identity ∑_{i ≤ r} (m choose i) · (n choose (r − i)) =104-- (m + n) choose r.105theorem choose.vandermonde (m n : Nat)106  shows ∀ r, Nat(r) → chooseConvolution(m, n, r, r + 1) = (m + n) choose r107proof108  induction m109  | zero =>110    intros r rNat111    have shape : 0 + n = n by ring112    rw [shape, chooseConvolution.zero_left]113    rfl114  | j + 1 using ih =>115    intros r rNat116    have split := natural.zero_or_successor at r117    cases split with isZero | isSucc118    . have one : 0 + 1 = 1 by compute119      rw [isZero, one, chooseConvolution.one]120      rw [choose.zero_right, choose.zero_right]121      rfl122    . obtain ⟨k, kNat, shape⟩ := isSucc123      have hk : succ(k) = k + 1124        symm125        exact add.right_one at k126      rw [shape, hk, chooseConvolution.pascal]127      have first := ih with k + 1, assumption128      have second := ih with k, kNat129      rw [first, second]130      have commute : j + 1 + n = (j + n) + 1 by ring131      rw [commute, choose.pascal]132      have aNat := choose.natural at j + n, k133      have bNat := choose.natural at j + n, k + 1134      ring135136theorem choose.vandermonde_at (m n r : Nat)137  shows chooseConvolution(m, n, r, r + 1) = (m + n) choose r138proof139  have all := choose.vandermonde at m, n140  exact all with r, assumption141142-- The convolution is symmetric in its two rows.143theorem chooseConvolution.symmetric (m n r : Nat)144  shows chooseConvolution(m, n, r, r + 1) = chooseConvolution(n, m, r, r + 1)145proof146  rw [choose.vandermonde_at, choose.vandermonde_at]147  have commute : m + n = n + m by ring148  rw commute149  rfl150151theorem choose.vandermonde_one (m n : Nat)152  shows chooseConvolution(m, n, 1, 2) = m + n153proof154  have two : 1 + 1 = 2 by compute155  rw ← two156  rw [choose.vandermonde_at, choose.one_right]157  rfl158159-- Partial sums of the squares of a row.160def chooseSquareSum (n k : Nat) → Nat161  | n, zero => 0162  | n, succ(k) => chooseSquareSum(n, k) + choose(n, k) * choose(n, k)163  descends k164165theorem chooseSquareSum.zero (n : Nat)166  shows chooseSquareSum(n, 0) = 0167proof168  simp [chooseSquareSum]169170theorem chooseSquareSum.succ (n k : Nat)171  shows chooseSquareSum(n, k + 1) =172    chooseSquareSum(n, k) + (n choose k) * (n choose k)173proof174  have hk : k + 1 = succ(k) := add.right_one with *175  rw hk176  simp [chooseSquareSum]177178theorem chooseSquareSum.natural (n k : Nat)179  shows Nat(chooseSquareSum(n, k))180proof181  induction k182  | zero =>183    rw chooseSquareSum.zero184    typecheck185  | j + 1 using ih =>186    rw chooseSquareSum.succ187    have cNat := choose.natural at n, j188    typecheck189190-- Below the diagonal the self-convolution of a row is the sum of its squares.191theorem chooseSquareSum.convolution (n k : Nat)192  requires le : k ≤ n + 1193  shows chooseConvolution(n, n, n, k) = chooseSquareSum(n, k)194proof195  induction k196  | zero =>197    intro le198    rw [chooseConvolution.zero, chooseSquareSum.zero]199    rfl200  | j + 1 using ih =>201    intro le202    have earlier : j ≤ n + 1 by arith203    have inner := ih with earlier204    rw [chooseConvolution.succ, chooseSquareSum.succ, inner]205    have jLe : j ≤ n by arith206    have mirror := choose.symmetric at n, j with jLe207    rw ← mirror208    rfl209210-- ∑_{k ≤ n} (n choose k)² = 2n choose n.211theorem choose.central_square_sum (n : Nat)212  shows chooseSquareSum(n, n + 1) = (2 * n) choose n213proof214  have le : n + 1 ≤ n + 1 by arith215  have convolution := chooseSquareSum.convolution at n, n + 1 with le216  rw ← convolution217  rw choose.vandermonde_at218  have double : n + n = 2 * n by ring219  rw double220  rfl221222theorem chooseSquareSum.monotone (n k d : Nat)223  shows chooseSquareSum(n, k) ≤ chooseSquareSum(n, k + d)224proof225  induction d226  | zero =>227    have shape : k + 0 = k by ring228    rw shape229    have sumNat := chooseSquareSum.natural at n, k230    exact LessEqual.reflexive at chooseSquareSum(n, k)231  | j + 1 using ih =>232    have shape : k + (j + 1) = (k + j) + 1 by ring233    rw [shape, chooseSquareSum.succ]234    have sumNat := chooseSquareSum.natural at n, k235    have sumNatJ := chooseSquareSum.natural at n, k + j236    have cNat := choose.natural at n, k + j237    have squareNat : Nat((n choose (k + j)) * (n choose (k + j))) by typecheck238    arith239240theorem chooseSquareSum.term_le (n k m : Nat)241  requires below : k < m242  shows (n choose k) * (n choose k) ≤ chooseSquareSum(n, m)243proof244  induction m245  | zero =>246    intro below247    have cNat := choose.natural at n, k248    have squareNat : Nat((n choose k) * (n choose k)) by typecheck249    arith250  | j + 1 using ih =>251    intro below252    rw chooseSquareSum.succ253    have sumNat := chooseSquareSum.natural at n, j254    have cNat := choose.natural at n, k255    have cNatJ := choose.natural at n, j256    have squareNat : Nat((n choose k) * (n choose k)) by typecheck257    have squareNatJ : Nat((n choose j) * (n choose j)) by typecheck258    have alternatives : k = j ∨ k ≠ j by tauto259    cases alternatives with same | different260    . rw same261      arith262    . have hj : j + 1 = succ(j) := add.right_one with *263      rw hj at below264      have strict := Less.of_successor_upper_ne with below, different265      have bound := ih with strict266      arith267268-- Every square of a row entry is bounded by the central coefficient.269theorem choose.square_le_central (n k : Nat)270  requires le : k ≤ n271  shows (n choose k) * (n choose k) ≤ (2 * n) choose n272proof273  rw ← choose.central_square_sum274  have below : k < n + 1 by arith275  exact chooseSquareSum.term_le with below276277theorem choose.le_central_of_le (n k : Nat)278  requires le : k ≤ n279  shows n choose k ≤ (2 * n) choose n280proof281  have square := choose.square_le_central with le282  have cNat := choose.natural at n, k283  have self := LessEqual.mul_self at n choose k284  have centralNat := choose.natural at 2 * n, n285  exact LessEqual.transitive with self, square286287-- The row sum is bounded by the sum of the squares.288theorem chooseRowSum.le_square_sum (n k : Nat)289  shows chooseRowSum(n, k) ≤ chooseSquareSum(n, k)290proof291  induction k292  | zero =>293    rw [chooseRowSum.zero, chooseSquareSum.zero]294    exact LessEqual.reflexive at 0295  | j + 1 using ih =>296    rw [chooseRowSum.succ, chooseSquareSum.succ]297    have cNat := choose.natural at n, j298    have self := LessEqual.mul_self at n choose j299    have rowNat := chooseRowSum.natural at n, j300    have squareNat := chooseSquareSum.natural at n, j301    exact LessEqual.add with ih, self302303-- The central binomial coefficient dominates 2 ^ n.304theorem choose.central_ge_pow (n : Nat)305  shows 2 ^ n ≤ (2 * n) choose n306proof307  rw [← choose.central_square_sum, ← chooseRowSum.full]308  exact chooseRowSum.le_square_sum at n, n + 1309