Grace/Cumulus/Combinatorics/Multinomial.g17

Imports

Declarations

trinomial def
trinomial.value theorem derivation
trinomial.natural theorem derivation
trinomial.factorial_form theorem derivation
trinomial.symmetric theorem derivation
trinomial.rotate theorem derivation
trinomial.swap_last theorem derivation
choose.mul_choose theorem derivation
choose.subset_chain theorem derivation
trinomial.zero_right theorem derivation
trinomial.zero_left theorem derivation
trinomial.positive theorem derivation
trinomial.recurrence theorem derivation
Source

1-- Trinomial coefficients (i + j + d)! / (i! j! d!) as products of binomial2-- coefficients: the factorial form, symmetry in the three parts, the3-- subset-of-a-subset identity, positivity, and the three-term recurrence4-- 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.Multinomial10import Stirling1112-- The number of ways to split i + j + d points into parts of sizes i, j, d.13def trinomial (i j d : Nat) : Nat := choose(i + j + d, i) * choose(j + d, j)1415theorem trinomial.value (i j d : Nat)16  shows trinomial(i, j, d) = ((i + j + d) choose i) * ((j + d) choose j)17proof18  simp [trinomial]1920theorem trinomial.natural (i j d : Nat)21  shows Nat(trinomial(i, j, d))22proof23  rw trinomial.value24  have aNat := choose.natural at i + j + d, i25  have bNat := choose.natural at j + d, j26  typecheck2728-- trinomial(i, j, d) · i! · j! · d! = (i + j + d)!.29theorem trinomial.factorial_form (i j d : Nat)30  shows trinomial(i, j, d) * (i! * j! * d!) = (i + j + d)!31proof32  rw trinomial.value33  have outerRow := choose.factorial at j + d34  have outer := outerRow with i, assumption35  have innerRow := choose.factorial at d36  have inner := innerRow with j, assumption37  have aNat := choose.natural at i + j + d, i38  have bNat := choose.natural at j + d, j39  have closedI := factorial.closed at i40  have closedJ := factorial.closed at j41  have closedD := factorial.closed at d42  have closedJD := factorial.closed at j + d43  ring [inner, outer]4445theorem trinomial.symmetric (i j d : Nat)46  shows trinomial(i, j, d) = trinomial(j, i, d)47proof48  have first := trinomial.factorial_form at i, j, d49  have second := trinomial.factorial_form at j, i, d50  have aNat := trinomial.natural at i, j, d51  have bNat := trinomial.natural at j, i, d52  have closedI := factorial.closed at i53  have closedJ := factorial.closed at j54  have closedD := factorial.closed at d55  have balanced : (i! * j! * d!) * trinomial(i, j, d) =56      (i! * j! * d!) * trinomial(j, i, d)57    ring [first, second]58  have nonzeroI := factorial.nonzero at i59  have nonzeroJ := factorial.nonzero at j60  have nonzeroIJ := mul.nonzero with nonzeroI, nonzeroJ61  have productNat : Nat(i! * j!) by typecheck62  have nonzero := mul.nonzero with nonzeroIJ, (factorial.nonzero at d)63  exact mul.left_cancel_positive with nonzero, balanced6465theorem trinomial.rotate (i j d : Nat)66  shows trinomial(i, j, d) = trinomial(j, d, i)67proof68  have first := trinomial.factorial_form at i, j, d69  have second := trinomial.factorial_form at j, d, i70  have aNat := trinomial.natural at i, j, d71  have bNat := trinomial.natural at j, d, i72  have closedI := factorial.closed at i73  have closedJ := factorial.closed at j74  have closedD := factorial.closed at d75  have balanced : (i! * j! * d!) * trinomial(i, j, d) =76      (i! * j! * d!) * trinomial(j, d, i)77    ring [first, second]78  have nonzeroI := factorial.nonzero at i79  have nonzeroJ := factorial.nonzero at j80  have nonzeroIJ := mul.nonzero with nonzeroI, nonzeroJ81  have productNat : Nat(i! * j!) by typecheck82  have nonzero := mul.nonzero with nonzeroIJ, (factorial.nonzero at d)83  exact mul.left_cancel_positive with nonzero, balanced8485theorem trinomial.swap_last (i j d : Nat)86  shows trinomial(i, j, d) = trinomial(i, d, j)87proof88  have first := trinomial.symmetric at i, j, d89  have second := trinomial.rotate at j, i, d90  rw [first, second]91  rfl9293-- Choosing i + j points and then i of them is choosing i points and then94-- j of the rest.95theorem choose.mul_choose (i j d : Nat)96  shows ((i + j + d) choose (i + j)) * ((i + j) choose i) = trinomial(i, j, d)97proof98  have form := trinomial.factorial_form at i, j, d99  have outerRow := choose.factorial at d100  have outer := outerRow with i + j, assumption101  have innerRow := choose.factorial at j102  have inner := innerRow with i, assumption103  have aNat := choose.natural at i + j + d, i + j104  have bNat := choose.natural at i + j, i105  have tNat := trinomial.natural at i, j, d106  have closedI := factorial.closed at i107  have closedJ := factorial.closed at j108  have closedD := factorial.closed at d109  have closedIJ := factorial.closed at i + j110  have balanced : (i! * j! * d!) *111      (((i + j + d) choose (i + j)) * ((i + j) choose i)) =112      (i! * j! * d!) * trinomial(i, j, d)113    ring [inner, outer, form]114  have nonzeroI := factorial.nonzero at i115  have nonzeroJ := factorial.nonzero at j116  have nonzeroIJ := mul.nonzero with nonzeroI, nonzeroJ117  have productNat : Nat(i! * j!) by typecheck118  have nonzero := mul.nonzero with nonzeroIJ, (factorial.nonzero at d)119  exact mul.left_cancel_positive with nonzero, balanced120121theorem choose.subset_chain (i j d : Nat)122  shows ((i + j + d) choose (i + j)) * ((i + j) choose i) =123    ((i + j + d) choose i) * ((j + d) choose j)124proof125  rw [choose.mul_choose, trinomial.value]126  rfl127128theorem trinomial.zero_right (i j : Nat)129  shows trinomial(i, j, 0) = (i + j) choose i130proof131  rw trinomial.value132  have shapeA : i + j + 0 = i + j by ring133  have shapeB : j + 0 = j by ring134  rw [shapeA, shapeB, choose.diagonal]135  have cNat := choose.natural at i + j, i136  ring137138theorem trinomial.zero_left (j d : Nat)139  shows trinomial(0, j, d) = (j + d) choose j140proof141  rw trinomial.value142  have shape : 0 + j + d = j + d by ring143  rw [shape, choose.zero_right]144  have cNat := choose.natural at j + d, j145  ring146147theorem trinomial.positive (i j d : Nat)148  shows 0 < trinomial(i, j, d)149proof150  rw trinomial.value151  have leI : i ≤ i + j + d by arith152  have leJ : j ≤ j + d by arith153  have first := choose.positive with leI154  have second := choose.positive with leJ155  have aNat := choose.natural at i + j + d, i156  have bNat := choose.natural at j + d, j157  exact Less.mul_positive with first, second158159-- Pascal's rule for three parts.160theorem trinomial.recurrence (i j d : Nat)161  shows trinomial(i + 1, j + 1, d + 1) =162    trinomial(i, j + 1, d + 1) + trinomial(i + 1, j, d + 1) +163    trinomial(i + 1, j + 1, d)164proof165  rw [trinomial.value, trinomial.value, trinomial.value, trinomial.value]166  have shapeA : i + 1 + (j + 1) + (d + 1) = (i + j + d + 2) + 1 by ring167  have shapeB : i + (j + 1) + (d + 1) = i + j + d + 2 by ring168  have shapeC : i + 1 + j + (d + 1) = i + j + d + 2 by ring169  have shapeD : i + 1 + (j + 1) + d = i + j + d + 2 by ring170  have shapeE : j + 1 + (d + 1) = (j + d + 1) + 1 by ring171  have shapeF : j + (d + 1) = j + d + 1 by ring172  have shapeG : j + 1 + d = j + d + 1 by ring173  rw [shapeA, shapeB, shapeC, shapeD, shapeE, shapeF, shapeG]174  have outer := choose.pascal at i + j + d + 2, i175  have inner := choose.pascal at j + d + 1, j176  rw [outer, inner]177  have aNat := choose.natural at i + j + d + 2, i178  have bNat := choose.natural at i + j + d + 2, i + 1179  have cNat := choose.natural at j + d + 1, j180  have dNat := choose.natural at j + d + 1, j + 1181  ring182