Grace/Cumulus/Combinatorics/FallingBounds.g17

Open in Workbench Download source

Imports

Catalan

Declarations

Source

1-- Bounds and divisibility for the falling factorial: it is at most n ^ m,2-- vanishes exactly above the diagonal, is a multiple of m!, splits at an3-- intermediate stage as a product of two falling factorials, divides n!,4-- and grows with its first argument5-- 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.FallingBounds11import Catalan1213theorem fallingFactorial.le_pow (n m : Nat)14  shows fallingFactorial(n, m) ≤ n ^ m15proof16  induction m17  | zero =>18    rw [fallingFactorial.zero, pow.zero]19    exact LessEqual.reflexive at 120  | j + 1 using ih =>21    rw [fallingFactorial.succ, pow.succ_right]22    have factor := sub.le_self at n, j23    have natural := fallingFactorial.natural at n, j24    have powNat := pow.closed at n, j25    have subNat := sub.closed at n, j26    exact LessEqual.mul with ih, factor2728theorem fallingFactorial.positive (n m : Nat)29  requires le : m ≤ n30  shows 0 < fallingFactorial(n, m)31proof32  have form := fallingFactorial.choose with le33  rw form34  have first := choose.positive with le35  have second := factorial.positive at m36  have cNat := choose.natural at n, m37  have closed := factorial.closed at m38  exact Less.mul_positive with first, second3940theorem fallingFactorial.eq_zero_iff (n m : Nat)41  shows fallingFactorial(n, m) = 0 ↔ n < m42proof43  constructor44  . intro zero45    by_contra notBelow46    have le := LessEqual.of_not_Less with notBelow47    have positive := fallingFactorial.positive with le48    rw zero at positive49    exact Less.irreflexive at 0 with positive50  . intro below51    exact fallingFactorial.of_Less with below5253theorem fallingFactorial.ne_zero_iff (n m : Nat)54  shows fallingFactorial(n, m) ≠ 0 ↔ m ≤ n55proof56  constructor57  . intro nonzero58    by_contra notLe59    have below := Less.of_not_LessEqual with notLe60    exact nonzero with (fallingFactorial.of_Less with below)61  . intro le62    intro zero63    have positive := fallingFactorial.positive with le64    rw zero at positive65    exact Less.irreflexive at 0 with positive6667theorem fallingFactorial.positive_iff (n m : Nat)68  shows 0 < fallingFactorial(n, m) ↔ m ≤ n69proof70  constructor71  . intro positive72    have natural := fallingFactorial.natural at n, m73    have nonzero := Less.ne_zero_of_positive with positive74    have iff := fallingFactorial.ne_zero_iff at n, m75    exact iff.forward with nonzero76  . intro le77    exact fallingFactorial.positive with le7879-- The factorial form holds without restriction: above the diagonal both80-- sides vanish.81theorem fallingFactorial.choose_mul (n k : Nat)82  shows fallingFactorial(n, k) = (n choose k) * k!83proof84  have alternatives := Less.or_LessEqual at n, k85  cases alternatives with below | le86  . have vanish := fallingFactorial.of_Less with below87    have vanishChoose := choose.above_diagonal with below88    rw [vanish, vanishChoose]89    have closed := factorial.closed at k90    ring91  . exact fallingFactorial.choose with le9293theorem choose.mul_factorial (n k : Nat)94  shows (n choose k) * k! = fallingFactorial(n, k)95proof96  symm97  exact fallingFactorial.choose_mul at n, k9899theorem fallingFactorial.factorial_divides (n m : Nat)100  shows m! ∣ fallingFactorial(n, m)101proof102  rw fallingFactorial.choose_mul103  have cNat := choose.natural at n, m104  have closed := factorial.closed at m105  witness n choose m106  ring107108-- Splitting the falling factorial at an intermediate stage.109theorem fallingFactorial.add (n m k : Nat)110  shows fallingFactorial(n, m + k) =111    fallingFactorial(n, m) * fallingFactorial(n - m, k)112proof113  induction k114  | zero =>115    have shape : m + 0 = m by ring116    rw [shape, fallingFactorial.zero]117    have natural := fallingFactorial.natural at n, m118    ring119  | j + 1 using ih =>120    have shape : m + (j + 1) = (m + j) + 1 by ring121    rw [shape, fallingFactorial.succ, ih, fallingFactorial.succ, sub.sub]122    have natural := fallingFactorial.natural at n, m123    have subNat := sub.closed at n, m124    have inner := fallingFactorial.natural at n - m, j125    have subNatJ := sub.closed at n - m, j126    ring127128theorem fallingFactorial.divides_add (n m k : Nat)129  shows fallingFactorial(n, m) ∣ fallingFactorial(n, m + k)130proof131  rw fallingFactorial.add132  have subNat := sub.closed at n, m133  have inner := fallingFactorial.natural at n - m, k134  have natural := fallingFactorial.natural at n, m135  witness fallingFactorial(n - m, k)136  rfl137138theorem fallingFactorial.divides_of_le (n m k : Nat)139  requires le : m ≤ k140  shows fallingFactorial(n, m) ∣ fallingFactorial(n, k)141proof142  obtain ⟨d, dNat, shape⟩ := le143  rw ← shape144  exact fallingFactorial.divides_add at n, m, d145146-- fallingFactorial(n, m) · (n − m)! = n! below the diagonal.147theorem fallingFactorial.mul_factorial_sub (n m : Nat)148  requires le : m ≤ n149  shows fallingFactorial(n, m) * (n - m)! = n!150proof151  obtain ⟨d, dNat, shape⟩ := le152  have difference : n - m = d153    rw ← shape154    exact sub.add_left at d, m155  rw [difference, ← shape]156  have row := fallingFactorial.mul_factorial at m157  exact row with d, dNat158159theorem fallingFactorial.divides_factorial (n m : Nat)160  requires le : m ≤ n161  shows fallingFactorial(n, m) ∣ n!162proof163  have form := fallingFactorial.mul_factorial_sub with le164  rw ← form165  have subNat := sub.closed at n, m166  have closed := factorial.closed at n - m167  have natural := fallingFactorial.natural at n, m168  witness (n - m)!169  rfl170171theorem fallingFactorial.le_factorial (n m : Nat)172  requires le : m ≤ n173  shows fallingFactorial(n, m) ≤ n!174proof175  have divides := fallingFactorial.divides_factorial with le176  have nonzero := factorial.nonzero at n177  have natural := fallingFactorial.natural at n, m178  have closed := factorial.closed at n179  exact divides.le with divides, nonzero180181theorem fallingFactorial.two (n : Nat)182  shows fallingFactorial(n, 2) = n * (n - 1)183proof184  have two : 1 + 1 = 2 by compute185  rw ← two186  rw [fallingFactorial.succ, fallingFactorial.one]187  rfl188189-- The falling factorial grows with its first argument.190theorem fallingFactorial.le_succ_left (n m : Nat)191  shows fallingFactorial(n, m) ≤ fallingFactorial(n + 1, m)192proof193  have split := natural.zero_or_successor at m194  cases split with isZero | isSucc195  . rw [isZero, fallingFactorial.zero, fallingFactorial.zero]196    exact LessEqual.reflexive at 1197  . obtain ⟨j, jNat, shape⟩ := isSucc198    have hj : succ(j) = j + 1199      symm200      exact add.right_one at j201    rw [shape, hj, fallingFactorial.succ, fallingFactorial.succ_succ]202    have natural := fallingFactorial.natural at n, j203    have subNat := sub.closed at n, j204    have factor : n - j ≤ n + 1205      have self := sub.le_self at n, j206      arith207    have scaled := LessEqual.mul_left at n - j, n + 1, fallingFactorial(n, j)208      with factor209    have commute : (n + 1) * fallingFactorial(n, j) =210      fallingFactorial(n, j) * (n + 1) by ring211    rw commute212    exact scaled213214theorem fallingFactorial.le_add_left (n d m : Nat)215  shows fallingFactorial(n, m) ≤ fallingFactorial(n + d, m)216proof217  induction d218  | zero =>219    have shape : n + 0 = n by ring220    rw shape221    have natural := fallingFactorial.natural at n, m222    exact LessEqual.reflexive at fallingFactorial(n, m)223  | j + 1 using ih =>224    have shape : n + (j + 1) = (n + j) + 1 by ring225    rw shape226    have step := fallingFactorial.le_succ_left at n + j, m227    have aNat := fallingFactorial.natural at n, m228    have bNat := fallingFactorial.natural at n + j, m229    have cNat := fallingFactorial.natural at n + j + 1, m230    exact LessEqual.transitive with ih, step231232theorem fallingFactorial.monotone_left (n k m : Nat)233  requires le : n ≤ k234  shows fallingFactorial(n, m) ≤ fallingFactorial(k, m)235proof236  obtain ⟨d, dNat, shape⟩ := le237  rw ← shape238  exact fallingFactorial.le_add_left at n, d, m239240-- The binomial coefficient is bounded by the power n ^ k.241theorem choose.le_pow_base (n k : Nat)242  shows n choose k ≤ n ^ k243proof244  have cNat := choose.natural at n, k245  have closed := factorial.closed at k246  have nonzero := factorial.nonzero at k247  have grow := LessEqual.le_mul_right at n choose k, k! with nonzero248  rw choose.mul_factorial at grow249  have bound := fallingFactorial.le_pow at n, k250  have natural := fallingFactorial.natural at n, k251  have powNat := pow.closed at n, k252  exact LessEqual.transitive with grow, bound253254-- There are no more injections than functions.255theorem injections.count_le (A B : Set)256  requires finiteA : Finite(A)257  requires finiteB : Finite(B)258  shows cardinality(injections(A, B)) ≤ cardinality(functionSpace(A, B))259proof260  have left := injections.count with finiteA, finiteB261  have right := functionSpace.count with finiteA, finiteB262  rw [left, right]263  have aNat := cardinality.nat with finiteA264  have bNat := cardinality.nat with finiteB265  exact fallingFactorial.le_pow at cardinality(B), cardinality(A)266