Multi-index binomial coefficients

For multi-indices d m : σ →₀ ℕ, the multi-index binomial coefficient is d.prod fun j k ↦ (m j).choose k = ∏ⱼ (mⱼ choose dⱼ). It is the coefficient by which the Hasse derivative ∂^d scales the monomial X^m.

Main results

• Finsupp.prod_choose_eq_zero: the coefficient vanishes unless d ≤ m.
• Finsupp.prod_choose_add_single: Pascal's rule in a single coordinate i.
• Finsupp.prod_choose_add_comm: ∏ⱼ (aⱼ + bⱼ choose aⱼ) is symmetric in a and b.
• Finsupp.prod_choose_le_two_pow_degree: the coefficient is at most 2 ^ |m|.

theorem Finsupp.prod_choose_eq_zero {σ : Type u_1} {d m : σ →₀ ℕ} (h : ¬d ≤ m) : (d.prod fun (j : σ) (k : ℕ) => (m j).choose k) = 0

The multi-index binomial coefficient ∏ⱼ (mⱼ choose dⱼ) vanishes unless d ≤ m.

theorem Finsupp.prod_choose_add_single {σ : Type u_1} (n d : σ →₀ ℕ) (i : σ) : (d.prod fun (j : σ) (k : ℕ) => ((n + single i 1) j).choose k) = (d.prod fun (j : σ) (k : ℕ) => (n j).choose k) + if d i = 0 then 0 else (d - single i 1).prod fun (j : σ) (k : ℕ) => (n j).choose k

Pascal's rule for the multi-index binomial coefficient, in the coordinate i: raising nᵢ by one adds the coefficient with dᵢ lowered by one, when dᵢ ≠ 0.

theorem Finsupp.prod_choose_add_comm {σ : Type u_1} (a b : σ →₀ ℕ) : (a.prod fun (j : σ) (k : ℕ) => (k + b j).choose k) = b.prod fun (j : σ) (k : ℕ) => (k + a j).choose k

The multi-index binomial coefficient ∏ⱼ (aⱼ + bⱼ choose aⱼ) is symmetric in a and b.

theorem Finsupp.prod_choose_le_two_pow_degree {σ : Type u_1} (d m : σ →₀ ℕ) : (d.prod fun (j : σ) (k : ℕ) => (m j).choose k) ≤ 2 ^ degree m

The multi-index binomial coefficient ∏ⱼ (mⱼ choose dⱼ) is at most 2 ^ |m|, where |m| = ∑ⱼ mⱼ is the degree of m.