Mathlib.Data.Nat.Choose

Multinomial and factorial identities for fixed-degree finite count vectors.

Bounds 1 core · 0 supporting For natural numbers k ≤ U ≤ M, the ratio of binomial coefficients C(U, k) / C(M, k) is at most (U/M)^k, in any linearly ordered field. ★ choose_div_choose_le_div_pow

A power bound for ratios of binomial coefficients

For natural numbers k ≤ U ≤ M, the ratio of binomial coefficients C(U, k) / C(M, k) is at most (U/M)^k, in any linearly ordered field. Equivalently, the probability that k draws without replacement from M items all land in a fixed subset of size U is at most the corresponding probability for draws with replacement.

Main results

choose_div_choose_le_div_pow — C(U, k) / C(M, k) ≤ (U/M)^k for k ≤ U ≤ M.

lemma choose_div_choose_le_div_pow reviewed

Causalean.Mathlib.Data.Nat.Choose

In an ordered field, for natural numbers U, M, and k with U ≤ M and k ≤ U, the ratio of their kth binomial coefficients is at most the kth power of U / M.

Formal statement

hypotheses

K :

Type*

Field K

LinearOrder K

IsStrictOrderedRing K

U M k :

ℕ

hUM :

U ≤ M

hk :

k ≤ U

conclusion

(U.choose k : K) / (M.choose k : K) ≤ ((U : K) / M) ^ k

Proof (Lean source)

lemma choose_div_choose_le_div_pow {K : Type*} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (U M k : ℕ) (hUM : U ≤ M) (hk : k ≤ U) : (U.choose k : K) / (M.choose k : K) ≤ ((U : K) / M) ^ k := by induction k with | zero => simp | succ k ih => have hkU : k < U := by omega have hkM : k < M := by omega have hMc : (0 : K) < (M.choose k : K) := by exact_mod_cast Nat.choose_pos hkM.le have hMcs : (0 : K) < (M.choose (k + 1) : K) := by exact_mod_cast Nat.choose_pos (by omega : k + 1 ≤ M) have hMk : (0 : K) < ((M - k : ℕ) : K) := by exact_mod_cast (by omega : 0 < M - k) have hMr : (0 : K) < M := by exact_mod_cast (by omega : 0 < M) have hUr : (U : K) ≤ M := by exact_mod_cast hUM have hrecU : (U.choose (k + 1) : K) * (k + 1 : K) = (U.choose k : K) * ((U - k : ℕ) : K) := by exact_mod_cast Nat.choose_succ_right_eq U k have hrecM : (M.choose (k + 1) : K) * (k + 1 : K) = (M.choose k : K) * ((M - k : ℕ) : K) := by exact_mod_cast Nat.choose_succ_right_eq M k have hratio : (U.choose (k + 1) : K) / (M.choose (k + 1) : K) = ((U.choose k : K) / (M.choose k : K)) * (((U - k : ℕ) : K) / ((M - k : ℕ) : K)) := by apply (div_eq_iff hMcs.ne').mpr field_simp nlinarith [hrecU, hrecM] have hfrac : ((U - k : ℕ) : K) / ((M - k : ℕ) : K) ≤ (U : K) / M := by rw [div_le_div_iff₀ hMk hMr, Nat.cast_sub hkU.le, Nat.cast_sub hkM.le] nlinarith rw [hratio, pow_succ] exact mul_le_mul (ih hkU.le) hfrac (by positivity) (by positivity)

Causalean.Mathlib.Data.Nat.Choose.choose_div_choose_le_div_pow · Causalean/Mathlib/Data/Nat/Choose/Bounds.lean:26

Multinomial 1 core · 0 supporting For real rates (a_i) indexed by a finite set and a total degree r, the sum over all count vectors (n_i) with Σ n_i = r of the products Π a_i^(n_i) / n_i! ★ factorial_countVector_fixed_degree_sum

The multinomial theorem in factorial-normalized form

For real rates (a_i) indexed by a finite set and a total degree r, the sum over all count vectors (n_i) with Σ n_i = r of the products Π a_i^(n_i) / n_i! equals (Σ a_i)^r / r!. This is the multinomial theorem divided through by r!, the form that appears when summing products of Poisson or exponential-series terms over a fixed total count.

Main results

* factorial_countVector_fixed_degree_sum — Σ over count vectors of total r of Π a_i^(n_i) / n_i! equals (Σ a_i)^r / r!.

lemma factorial_countVector_fixed_degree_sum reviewed

Causalean.Mathlib.Data.Nat.Choose

For a finite coordinate type, real coordinate rates, and a total degree, the sum, over all vectors of natural counts adding up to that degree, of the product over coordinates of rate to the power count divided by count factorial, equals the degree-th power of the sum of the rates divided by the factorial of the degree.

Formal statement

hypotheses

I :

Type*

Fintype I

DecidableEq I

rate :

I → ℝ

r :

ℕ

conclusion

(∑ counts ∈ (Finset.univ : Finset I).piAntidiag r, ∏ i : I, rate i ^ counts i / (counts i).factorial)

= (∑ i : I, rate i) ^ r / (r.factorial : ℝ)

Proof (Lean source)

lemma factorial_countVector_fixed_degree_sum {I : Type*} [Fintype I] [DecidableEq I] (rate : I → ℝ) (r : ℕ) : (∑ counts ∈ (Finset.univ : Finset I).piAntidiag r, ∏ i : I, rate i ^ counts i / (counts i).factorial) = (∑ i : I, rate i) ^ r / (r.factorial : ℝ) := by classical rw [Finset.sum_pow_eq_sum_piAntidiag, Finset.sum_div] apply Finset.sum_congr rfl intro counts hc have hsum : ∑ i : I, counts i = r := (Finset.mem_piAntidiag.mp hc).1 have hspec : (∏ i : I, ((counts i).factorial : ℝ)) * (Nat.multinomial Finset.univ counts : ℝ) = (r.factorial : ℝ) := by exact_mod_cast (hsum ▸ Nat.multinomial_spec Finset.univ counts) have hprod : (∏ i : I, ((counts i).factorial : ℝ)) ≠ 0 := by positivity rw [Finset.prod_div_distrib] apply (div_eq_div_iff hprod (by positivity)).mpr rw [← hspec] ring

Causalean.Mathlib.Data.Nat.Choose.factorial_countVector_fixed_degree_sum · Causalean/Mathlib/Data/Nat/Choose/Multinomial.lean:28