Grace/Cumulus/Combinatorics/Catalan.g17

Open in Workbench Download source

Imports

Vandermonde

Declarations

Source

1-- The central binomial coefficients and the Catalan numbers: positivity,2-- parity, the step 2n choose n → 2n + 2 choose n + 1 in product form, the3-- closed form (n + 1) · catalan(n) = 2n choose n, the recurrence4-- (n + 2) · catalan(n + 1) = 2(2n + 1) · catalan(n), monotonicity, and the5-- bound catalan(n) ≤ 4 ^ n6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Combinatorics.Catalan12import Vandermonde1314theorem choose.central_positive (n : Nat)15  shows 0 < (2 * n) choose n16proof17  have le : n ≤ 2 * n by arith18  exact choose.positive with le1920theorem choose.central_le_pow (n : Nat)21  shows (2 * n) choose n ≤ 4 ^ n22proof23  have bound := choose.le_pow at 2 * n, n24  have square := pow.mul_exponent at 2, 2, n25  have four : 2 ^ 2 = 4 by compute26  rw four at square27  rw square28  exact bound2930-- Pascal's rule and symmetry: 2n + 2 choose n + 1 = 2 · (2n + 1 choose n).31theorem choose.central_double (n : Nat)32  shows (2 * (n + 1)) choose (n + 1) = 2 * ((n + 1 + n) choose (n + 1))33proof34  have shape : 2 * (n + 1) = (n + 1 + n) + 1 by ring35  rw [shape, choose.pascal]36  have mirror := choose.add_symmetric at n + 1, n37  rw mirror38  have cNat := choose.natural at n + 1 + n, n + 139  ring4041theorem choose.central_even (n : Nat)42  shows Even((2 * (n + 1)) choose (n + 1))43proof44  rw choose.central_double45  have cNat := choose.natural at n + 1 + n, n + 146  exact Even.two_mul at (n + 1 + n) choose (n + 1)4748-- The step between consecutive central coefficients, in product form.49theorem choose.central_step (n : Nat)50  shows (n + 1) * ((2 * (n + 1)) choose (n + 1)) =51    2 * (2 * n + 1) * ((2 * n) choose n)52proof53  rw choose.central_double54  have absorb := choose.absorption_at at 2 * n, n55  have shape : 2 * n + 1 = n + 1 + n by ring56  rw shape at absorb57  have cNat := choose.natural at n + 1 + n, n + 158  have centralNat := choose.natural at 2 * n, n59  rw shape60  ring [absorb]6162-- The entry next to the centre:63-- (n + 1) · (2n choose n + 1) = n · (2n choose n).64theorem choose.central_next (n : Nat)65  shows (n + 1) * ((2 * n) choose (n + 1)) = n * ((2 * n) choose n)66proof67  have step := choose.central_step at n68  rw choose.central_double at step69  have inner := choose.pascal at 2 * n, n70  have shape : 2 * n + 1 = n + 1 + n by ring71  rw shape at inner72  rw inner at step73  have aNat := choose.natural at 2 * n, n74  have bNat := choose.natural at 2 * n, n + 175  have balanced : 2 * ((n + 1) * ((2 * n) choose (n + 1))) +76      2 * (n + 1) * ((2 * n) choose n) =77      2 * (n * ((2 * n) choose n)) + 2 * (n + 1) * ((2 * n) choose n)78    ring [step]79  have cancelled := add.right_cancel with balanced80  have twoPositive : 0 < 2 by arith81  have two := Less.ne_zero_of_positive with twoPositive82  exact mul.left_cancel_positive with two, cancelled8384theorem choose.central_next_lt (n : Nat)85  shows (2 * n) choose (n + 1) < (2 * n) choose n86proof87  have next := choose.central_next at n88  have aNat := choose.natural at 2 * n, n89  have bNat := choose.natural at 2 * n, n + 190  have positive := choose.central_positive at n91  have strict : n * ((2 * n) choose n) < (n + 1) * ((2 * n) choose n)92    have below : n < n + 1 by arith93    have nonzero := Less.ne_zero_of_positive with positive94    exact Less.mul_right with nonzero, below95  rw ← next at strict96  have gapPositive : 0 < n + 1 by arith97  have gap := Less.ne_zero_of_positive with gapPositive98  exact Less.mul_left_cancel_positive with gap, strict99100theorem choose.central_monotone (n : Nat)101  shows (2 * n) choose n ≤ (2 * (n + 1)) choose (n + 1)102proof103  have step := choose.central_step at n104  have aNat := choose.natural at 2 * n, n105  have bNat := choose.natural at 2 * (n + 1), n + 1106  have coefficient : n + 1 ≤ 2 * (2 * n + 1) by arith107  have scaled := LessEqual.mul_right at n + 1, 2 * (2 * n + 1), (2 * n) choose n108    with coefficient109  rw ← step at scaled110  have nonzeroPositive : 0 < n + 1 by arith111  have nonzero := Less.ne_zero_of_positive with nonzeroPositive112  exact LessEqual.mul_left_cancel_positive with nonzero, scaled113114theorem choose.central_strict (n : Nat)115  shows (2 * n) choose n < (2 * (n + 1)) choose (n + 1)116proof117  have step := choose.central_step at n118  have aNat := choose.natural at 2 * n, n119  have bNat := choose.natural at 2 * (n + 1), n + 1120  have positive := choose.central_positive at n121  have nonzero := Less.ne_zero_of_positive with positive122  have coefficient : n + 1 < 2 * (2 * n + 1) by arith123  have scaled := Less.mul_right at n + 1, 2 * (2 * n + 1), (2 * n) choose n124    with nonzero, coefficient125  rw ← step at scaled126  have gapPositive : 0 < n + 1 by arith127  have gap := Less.ne_zero_of_positive with gapPositive128  exact Less.mul_left_cancel_positive with gap, scaled129130-- The Catalan numbers in closed form, 2n choose n − 2n choose n + 1.131def catalan (n : Nat) : Nat := ((2 * n) choose n) - ((2 * n) choose (n + 1))132133theorem catalan.value (n : Nat)134  shows catalan(n) = ((2 * n) choose n) - ((2 * n) choose (n + 1))135proof136  simp [catalan]137138theorem catalan.zero139  shows catalan(0) = 1140proof141  compute142143theorem catalan.one144  shows catalan(1) = 1145proof146  compute147148theorem catalan.two149  shows catalan(2) = 2150proof151  compute152153theorem catalan.three154  shows catalan(3) = 5155proof156  compute157158theorem catalan.four159  shows catalan(4) = 14160proof161  compute162163theorem catalan.five164  shows catalan(5) = 42165proof166  compute167168theorem catalan.natural (n : Nat)169  shows Nat(catalan(n))170proof171  rw catalan.value172  have aNat := choose.natural at 2 * n, n173  have bNat := choose.natural at 2 * n, n + 1174  exact sub.closed at (2 * n) choose n, (2 * n) choose (n + 1)175176-- (n + 1) · catalan(n) = 2n choose n.177theorem catalan.closed (n : Nat)178  shows (n + 1) * catalan(n) = (2 * n) choose n179proof180  rw [catalan.value, sub.mul_left, choose.central_next]181  have cNat := choose.natural at 2 * n, n182  have expand : (n + 1) * ((2 * n) choose n) =183    n * ((2 * n) choose n) + ((2 * n) choose n) by ring184  rw expand185  exact sub.add_left at (2 * n) choose n, n * ((2 * n) choose n)186187theorem catalan.positive (n : Nat)188  shows 0 < catalan(n)189proof190  have closed := catalan.closed at n191  have central := choose.central_positive at n192  rw ← closed at central193  have cNat := catalan.natural at n194  have iff := mul.positive_iff at n + 1, catalan(n)195  have both := iff.forward with central196  exact both.right197198theorem catalan.ge_one (n : Nat)199  shows 1 ≤ catalan(n)200proof201  have positive := catalan.positive at n202  have cNat := catalan.natural at n203  arith204205theorem catalan.le_central (n : Nat)206  shows catalan(n) ≤ (2 * n) choose n207proof208  rw catalan.value209  have aNat := choose.natural at 2 * n, n210  have bNat := choose.natural at 2 * n, n + 1211  exact sub.le_self at (2 * n) choose n, (2 * n) choose (n + 1)212213theorem catalan.le_pow (n : Nat)214  shows catalan(n) ≤ 4 ^ n215proof216  have first := catalan.le_central at n217  have second := choose.central_le_pow at n218  have cNat := catalan.natural at n219  have centralNat := choose.natural at 2 * n, n220  have powNat := pow.closed at 4, n221  exact LessEqual.transitive with first, second222223-- Segner's recurrence in product form: (n + 2) · C(n + 1) = 2(2n + 1) · C(n).224theorem catalan.recurrence (n : Nat)225  shows (n + 2) * catalan(n + 1) = 2 * (2 * n + 1) * catalan(n)226proof227  have closedNext := catalan.closed at n + 1228  have closed := catalan.closed at n229  have step := choose.central_step at n230  rw [← closedNext, ← closed] at step231  have aNat := catalan.natural at n232  have bNat := catalan.natural at n + 1233  have balanced : (n + 1) * ((n + 2) * catalan(n + 1)) =234    (n + 1) * (2 * (2 * n + 1) * catalan(n)) by ring [step]235  have nonzeroPositive : 0 < n + 1 by arith236  have nonzero := Less.ne_zero_of_positive with nonzeroPositive237  exact mul.left_cancel_positive with nonzero, balanced238239theorem catalan.monotone (n : Nat)240  shows catalan(n) ≤ catalan(n + 1)241proof242  have recurrence := catalan.recurrence at n243  have aNat := catalan.natural at n244  have bNat := catalan.natural at n + 1245  have coefficient : n + 2 ≤ 2 * (2 * n + 1) by arith246  have scaled := LessEqual.mul_right at n + 2, 2 * (2 * n + 1), catalan(n)247    with coefficient248  rw ← recurrence at scaled249  have nonzeroPositive : 0 < n + 2 by arith250  have nonzero := Less.ne_zero_of_positive with nonzeroPositive251  exact LessEqual.mul_left_cancel_positive with nonzero, scaled252253theorem catalan.strict (n : Nat)254  shows catalan(n + 1) < catalan(n + 2)255proof256  have recurrence := catalan.recurrence at n + 1257  have aNat := catalan.natural at n + 1258  have bNat := catalan.natural at n + 1 + 1259  have positive := catalan.positive at n + 1260  have nonzero := Less.ne_zero_of_positive with positive261  have coefficient : n + 1 + 2 < 2 * (2 * (n + 1) + 1) by arith262  have scaled := Less.mul_right at n + 1 + 2, 2 * (2 * (n + 1) + 1),263    catalan(n + 1) with nonzero, coefficient264  rw ← recurrence at scaled265  have shape : n + 1 + 1 = n + 2 by ring266  rw shape at scaled267  have gapPositive : 0 < n + 1 + 2 by arith268  have gap := Less.ne_zero_of_positive with gapPositive269  exact Less.mul_left_cancel_positive with gap, scaled270271theorem catalan.le_of_le (m d : Nat)272  shows catalan(m) ≤ catalan(m + d)273proof274  induction d275  | zero =>276    have shape : m + 0 = m by ring277    rw shape278    have cNat := catalan.natural at m279    exact LessEqual.reflexive at catalan(m)280  | j + 1 using ih =>281    have shape : m + (j + 1) = (m + j) + 1 by ring282    rw shape283    have step := catalan.monotone at m + j284    have aNat := catalan.natural at m285    have bNat := catalan.natural at m + j286    have cNat := catalan.natural at m + j + 1287    exact LessEqual.transitive with ih, step288289theorem catalan.two_le (n : Nat)290  shows 2 ≤ catalan(n + 2)291proof292  have bound := catalan.le_of_le at 2, n293  have shape : 2 + n = n + 2 by ring294  rw [shape, catalan.two] at bound295  exact bound296297-- The convolution ∑_{i < k} catalan(i) · catalan(n − i) of Segner's298-- recurrence; the instances below are checked by computation.299def catalanConvolution (n k : Nat) → Nat300  | n, zero => 0301  | n, succ(k) => catalanConvolution(n, k) + catalan(k) * catalan(sub(n, k))302  descends k303304theorem catalanConvolution.zero (n : Nat)305  shows catalanConvolution(n, 0) = 0306proof307  simp [catalanConvolution]308309theorem catalanConvolution.succ (n k : Nat)310  shows catalanConvolution(n, k + 1) =311    catalanConvolution(n, k) + catalan(k) * catalan(n - k)312proof313  have hk : k + 1 = succ(k) := add.right_one with *314  rw hk315  simp [catalanConvolution]316317theorem catalanConvolution.natural (n k : Nat)318  shows Nat(catalanConvolution(n, k))319proof320  induction k321  | zero =>322    rw catalanConvolution.zero323    typecheck324  | j + 1 using ih =>325    rw catalanConvolution.succ326    have aNat := catalan.natural at j327    have subNat := sub.closed at n, j328    have bNat := catalan.natural at n - j329    typecheck330331theorem catalan.convolution_two332  shows catalan(3) = catalanConvolution(2, 3)333proof334  compute335336theorem catalan.convolution_three337  shows catalan(4) = catalanConvolution(3, 4)338proof339  compute340341theorem catalan.convolution_four342  shows catalan(5) = catalanConvolution(4, 5)343proof344  compute345