Combinatorial coefficient formulas and nonnegativity (Theorems 2 and 3)

This file formalizes Theorems 2 and 3 of the Chebyshev-quotient / Demazure-multiplicity paper: explicit Cauchy-product and matrix-inverse formulas for the generating-function coefficients and their nonnegativity via a Dyck-path counting model.

Definition 1: Chebyshev-type polynomials

noncomputable def Biswal.Theorem23.polyP (R : Type u_1) [CommRing R] : ℕ → Polynomial R

The Chebyshev-type polynomial sequence P n over a commutative ring, defined by P 0 = P 1 = 1 and P (n + 2) = P (n + 1) - X * P n.

Equations

• Biswal.Theorem23.polyP R 0 = 1
• Biswal.Theorem23.polyP R 1 = 1
• Biswal.Theorem23.polyP R n.succ.succ = Biswal.Theorem23.polyP R (n + 1) - Polynomial.X * Biswal.Theorem23.polyP R n

theorem Biswal.Theorem23.polyP_zero (R : Type u_1) [CommRing R] : polyP R 0 = 1

theorem Biswal.Theorem23.polyP_one (R : Type u_1) [CommRing R] : polyP R 1 = 1

theorem Biswal.Theorem23.polyP_succ_succ (R : Type u_1) [CommRing R] (n : ℕ) : polyP R (n + 2) = polyP R (n + 1) - Polynomial.X * polyP R n

Definition 2: Partition polynomial

noncomputable def Biswal.Theorem23.partitionPoly (R : Type u_1) [CommRing R] {s : ℕ} (ξ : s.Partition) : Polynomial R

The partition polynomial of ξ: the product of polyP R over the parts of ξ.

Equations

• Biswal.Theorem23.partitionPoly R ξ = (Multiset.map (Biswal.Theorem23.polyP R) ξ.parts).prod

Definition 3: Generating function

noncomputable def Biswal.Theorem23.genFun (K : Type u_1) [Field K] (m μ : ℕ) {s : ℕ} (ξ : s.Partition) : PowerSeries K

The generating function attached to ξ with parameters m and μ, as a power series.

Equations

• Biswal.Theorem23.genFun K m μ ξ = ↑(Biswal.Theorem23.polyP K (m - μ % m - 1) * Biswal.Theorem23.partitionPoly K ξ) * (↑(Biswal.Theorem23.polyP K m) ^ (μ / m + 1))⁻¹

noncomputable def Biswal.Theorem23.genFunCoeff (K : Type u_1) [Field K] (m μ r : ℕ) {s : ℕ} (ξ : s.Partition) : K

The r-th coefficient of the generating function genFun K m μ ξ.

Equations

• Biswal.Theorem23.genFunCoeff K m μ r ξ = (PowerSeries.coeff r) (Biswal.Theorem23.genFun K m μ ξ)

Definition 4: Count of maximal parts

def Biswal.Theorem23.countMaxParts (m : ℕ) {s : ℕ} (ξ : s.Partition) : ℕ

The number of parts of ξ equal to m.

Equations

• Biswal.Theorem23.countMaxParts m ξ = Multiset.count m ξ.parts

Definition 5: Reduced parameters

def Biswal.Theorem23.nonMaxParts (m : ℕ) {s : ℕ} (ξ : s.Partition) : Multiset ℕ

The multiset of parts of ξ strictly less than m.

Equations

• Biswal.Theorem23.nonMaxParts m ξ = Multiset.filter (fun (x : ℕ) => x < m) ξ.parts

noncomputable def Biswal.Theorem23.nonMaxPartsPoly (K : Type u_1) [CommRing K] (m : ℕ) {s : ℕ} (ξ : s.Partition) : Polynomial K

The product of polyP K over the parts of ξ strictly less than m.

Equations

• Biswal.Theorem23.nonMaxPartsPoly K m ξ = (Multiset.map (Biswal.Theorem23.polyP K) (Biswal.Theorem23.nonMaxParts m ξ)).prod

def Biswal.Theorem23.alphaMultiset (m μ : ℕ) {s : ℕ} (ξ : s.Partition) : Multiset ℕ

The multiset of reduced indices m - μ % m - 1 prepended to the non-maximal parts of ξ.

Equations

• Biswal.Theorem23.alphaMultiset m μ ξ = (m - μ % m - 1) ::ₘ Biswal.Theorem23.nonMaxParts m ξ

def Biswal.Theorem23.reducedK (m μ : ℕ) {s : ℕ} (ξ : s.Partition) : ℕ

The reduced exponent μ / m + 1 - countMaxParts m ξ.

Equations

• Biswal.Theorem23.reducedK m μ ξ = μ / m + 1 - Biswal.Theorem23.countMaxParts m ξ

def Biswal.Theorem23.alphaCount (m μ : ℕ) {s : ℕ} (ξ : s.Partition) : ℕ

The number of entries in alphaMultiset m μ ξ.

Equations

• Biswal.Theorem23.alphaCount m μ ξ = (Biswal.Theorem23.alphaMultiset m μ ξ).card

noncomputable def Biswal.Theorem23.alphaProd (K : Type u_1) [CommRing K] (m μ : ℕ) {s : ℕ} (ξ : s.Partition) : Polynomial K

The product of polyP K over the entries of alphaMultiset m μ ξ.

Equations

• Biswal.Theorem23.alphaProd K m μ ξ = (Multiset.map (Biswal.Theorem23.polyP K) (Biswal.Theorem23.alphaMultiset m μ ξ)).prod

noncomputable def Biswal.Theorem23.alphaValues (m μ : ℕ) {s : ℕ} (ξ : s.Partition) : List ℕ

The entries of alphaMultiset m μ ξ as a list.

Equations

• Biswal.Theorem23.alphaValues m μ ξ = (Biswal.Theorem23.alphaMultiset m μ ξ).toList

Basic properties of polyP

theorem Biswal.Theorem23.polyP_constantCoeff (R : Type u_1) [CommRing R] (n : ℕ) : (polyP R n).coeff 0 = 1

theorem Biswal.Theorem23.polyP_coe_constantCoeff_ne_zero (K : Type u_1) [Field K] (m : ℕ) : PowerSeries.constantCoeff ↑(polyP K m) ≠ 0

theorem Biswal.Theorem23.polyP_coe_pow_constantCoeff_ne_zero (K : Type u_1) [Field K] (m k : ℕ) : PowerSeries.constantCoeff (↑(polyP K m) ^ k) ≠ 0

Definition 6: Coefficients of 1/p_m(x)

noncomputable def Biswal.Theorem23.bCoeff (K : Type u_1) [Field K] (m u : ℕ) : K

The u-th coefficient of the power-series inverse 1 / polyP K m.

Equations

• Biswal.Theorem23.bCoeff K m u = (PowerSeries.coeff u) (↑(Biswal.Theorem23.polyP K m))⁻¹

Definition 7: Coefficients of p_a · p_b / p_m

noncomputable def Biswal.Theorem23.dCoeff (K : Type u_1) [Field K] (m a b u : ℕ) : K

The u-th coefficient of the power series polyP K a * polyP K b / polyP K m.

Equations

• Biswal.Theorem23.dCoeff K m a b u = (PowerSeries.coeff u) (↑(Biswal.Theorem23.polyP K a * Biswal.Theorem23.polyP K b) * (↑(Biswal.Theorem23.polyP K m))⁻¹)

Reduced form of the generating function

theorem Biswal.Theorem23.partitionPoly_eq_pow_mul_nonMax (K : Type u_1) [CommRing K] (m : ℕ) {s : ℕ} (ξ : s.Partition) (h_parts : ∀ i ∈ ξ.parts, i ≤ m) : partitionPoly K ξ = polyP K m ^ countMaxParts m ξ * nonMaxPartsPoly K m ξ

theorem Biswal.Theorem23.alphaProd_eq_mul_nonMax (K : Type u_1) [CommRing K] (m μ : ℕ) {s : ℕ} (ξ : s.Partition) : alphaProd K m μ ξ = polyP K (m - μ % m - 1) * nonMaxPartsPoly K m ξ

theorem Biswal.Theorem23.ps_inv_pow_eq (K : Type u_1) [Field K] (φ : PowerSeries K) (k : ℕ) : (φ ^ k)⁻¹ = φ⁻¹ ^ k

theorem Biswal.Theorem23.pow_mul_pow_inv_cancel (K : Type u_1) [Field K] (P : PowerSeries K) (t e : ℕ) (hte : t ≤ e) (hP : PowerSeries.constantCoeff P ≠ 0) : P ^ t * (P ^ e)⁻¹ = (P ^ (e - t))⁻¹

theorem Biswal.Theorem23.genFun_eq_reduced (K : Type u_1) [Field K] (m μ : ℕ) {s : ℕ} (ξ : s.Partition) (_hm : 2 ≤ m) (h_parts : ∀ i ∈ ξ.parts, i ≤ m) (hk : countMaxParts m ξ ≤ μ / m + 1) : genFun K m μ ξ = ↑(alphaProd K m μ ξ) * (↑(polyP K m) ^ reducedK m μ ξ)⁻¹

Coefficient formula for polyP

theorem Biswal.Theorem23.polyP_coeff (R : Type u_1) [CommRing R] (n j : ℕ) : (polyP R n).coeff j = (-1) ^ j * ↑((n - j).choose j)

theorem Biswal.Theorem23.D_coeff_mk (K : Type u_1) [Field K] (m a b : ℕ) : ↑(polyP K a * polyP K b) * (↑(polyP K m))⁻¹ = PowerSeries.mk (dCoeff K m a b)

Theorem 2: Cauchy product form

theorem Biswal.Theorem23.thm_comb_cauchy (K : Type u_1) [Field K] (m μ : ℕ) {s : ℕ} (ξ : s.Partition) (hm : 2 ≤ m) (h_parts : ∀ i ∈ ξ.parts, i ≤ m) (hk : countMaxParts m ξ ≤ μ / m + 1) (r : ℕ) : genFunCoeff K m μ r ξ = (PowerSeries.coeff r) (↑(alphaProd K m μ ξ) * (↑(polyP K m))⁻¹ ^ reducedK m μ ξ)

Theorem 2: Explicit summation formula

theorem Biswal.Theorem23.cauchy_product_as_fin_prod (m μ : ℕ) {s : ℕ} (ξ : s.Partition) (r : ℕ) : have αs := alphaValues m μ ξ; have L1 := αs.length; have k := reducedK m μ ξ; (PowerSeries.coeff r) (↑(alphaProd ℚ m μ ξ) * (↑(polyP ℚ m))⁻¹ ^ k) = ∑ f ∈ Finset.Nat.antidiagonalTuple (L1 + k) r, (∏ i : Fin L1, (-1) ^ f (Fin.castAdd k i) * ↑((αs.getD (↑i) 0 - f (Fin.castAdd k i)).choose (f (Fin.castAdd k i)))) * ∏ ν : Fin k, bCoeff ℚ m (f (Fin.natAdd L1 ν))

theorem Biswal.Theorem23.thm_comb (m μ : ℕ) {s : ℕ} (ξ : s.Partition) (hm : 2 ≤ m) (h_parts : ∀ i ∈ ξ.parts, i ≤ m) (hk : countMaxParts m ξ ≤ μ / m + 1) (r : ℕ) : have αs := alphaValues m μ ξ; have L1 := αs.length; have k := reducedK m μ ξ; genFunCoeff ℚ m μ r ξ = ∑ f ∈ Finset.Nat.antidiagonalTuple (L1 + k) r, (∏ i : Fin L1, (-1) ^ f (Fin.castAdd k i) * ↑((αs.getD (↑i) 0 - f (Fin.castAdd k i)).choose (f (Fin.castAdd k i)))) * ∏ ν : Fin k, bCoeff ℚ m (f (Fin.natAdd L1 ν))

Theorem 3: Part (i) - Factorization

theorem Biswal.Theorem23.coe_prod_mul_inv_pow_eq_prod (m k : ℕ) (pairs : Fin k → ℕ × ℕ) : ↑(∏ ν : Fin k, polyP ℚ (pairs ν).1 * polyP ℚ (pairs ν).2) * (↑(polyP ℚ m))⁻¹ ^ k = ∏ ν : Fin k, ↑(polyP ℚ (pairs ν).1 * polyP ℚ (pairs ν).2) * (↑(polyP ℚ m))⁻¹

theorem Biswal.Theorem23.thm_manifest_factorization (m μ : ℕ) {s : ℕ} (ξ : s.Partition) (hm : 2 ≤ m) (h_parts : ∀ i ∈ ξ.parts, i ≤ m) (hk_nonneg : countMaxParts m ξ ≤ μ / m + 1) (k : ℕ) (hk_eq : k = reducedK m μ ξ) (pairs : Fin k → ℕ × ℕ) (h_bound : ∀ (ν : Fin k), (pairs ν).1 ≤ m - 1 ∧ (pairs ν).2 ≤ m - 1 ∧ (pairs ν).1 + (pairs ν).2 ≤ m - 1) (h_factor : alphaProd ℚ m μ ξ = ∏ ν : Fin k, polyP ℚ (pairs ν).1 * polyP ℚ (pairs ν).2) : genFun ℚ m μ ξ = ∏ ν : Fin k, PowerSeries.mk (dCoeff ℚ m (pairs ν).1 (pairs ν).2)

Theorem 3: Part (i), coefficient form

theorem Biswal.Theorem23.coeff_prod_mk_eq_sum_antidiag (k r : ℕ) (g : Fin k → ℕ → ℚ) : (PowerSeries.coeff r) (∏ ν : Fin k, PowerSeries.mk (g ν)) = ∑ f ∈ Finset.Nat.antidiagonalTuple k r, ∏ ν : Fin k, g ν (f ν)

theorem Biswal.Theorem23.thm_manifest_coeff_formula (m μ : ℕ) {s : ℕ} (ξ : s.Partition) (hm : 2 ≤ m) (h_parts : ∀ i ∈ ξ.parts, i ≤ m) (hk_nonneg : countMaxParts m ξ ≤ μ / m + 1) (k : ℕ) (hk_eq : k = reducedK m μ ξ) (pairs : Fin k → ℕ × ℕ) (h_bound : ∀ (ν : Fin k), (pairs ν).1 ≤ m - 1 ∧ (pairs ν).2 ≤ m - 1 ∧ (pairs ν).1 + (pairs ν).2 ≤ m - 1) (h_factor : alphaProd ℚ m μ ξ = ∏ ν : Fin k, polyP ℚ (pairs ν).1 * polyP ℚ (pairs ν).2) (r : ℕ) : genFunCoeff ℚ m μ r ξ = ∑ f ∈ Finset.Nat.antidiagonalTuple k r, ∏ ν : Fin k, dCoeff ℚ m (pairs ν).1 (pairs ν).2 (f ν)

Theorem 3: Part (ii) - Nonnegativity of dCoeff

theorem Biswal.Theorem23.polyP_map_intCast (n : ℕ) : polyP ℚ n = Polynomial.map (Int.castRingHom ℚ) (polyP ℤ n)

theorem Biswal.Theorem23.polyP_coe_int_constantCoeff (m : ℕ) : PowerSeries.constantCoeff ↑(polyP ℤ m) = 1

theorem Biswal.Theorem23.polyP_map_coe_eq (m : ℕ) : (PowerSeries.map (Int.castRingHom ℚ)) ↑(polyP ℤ m) = ↑(polyP ℚ m)

theorem Biswal.Theorem23.polyP_inv_map_eq (m : ℕ) : (PowerSeries.map (Int.castRingHom ℚ)) ((↑(polyP ℤ m)).invOfUnit 1) = (↑(polyP ℚ m))⁻¹

theorem Biswal.Theorem23.polyP_inv_coeff_is_int (m u : ℕ) : ∃ (z : ℤ), (PowerSeries.coeff u) (↑(polyP ℚ m))⁻¹ = ↑z

theorem Biswal.Theorem23.polyP_prod_coeff_is_int (a b u : ℕ) : ∃ (z : ℤ), (PowerSeries.coeff u) ↑(polyP ℚ a * polyP ℚ b) = ↑z

theorem Biswal.Theorem23.sum_int_cast_of_each_int {ι : Type u_1} (s : Finset ι) (f : ι → ℚ) (hf : ∀ i ∈ s, ∃ (z : ℤ), f i = ↑z) : ∃ (z : ℤ), ∑ i ∈ s, f i = ↑z

theorem Biswal.Theorem23.int_coeff_mul_int_coeff (α β : PowerSeries ℚ) (hα : ∀ (n : ℕ), ∃ (z : ℤ), (PowerSeries.coeff n) α = ↑z) (hβ : ∀ (n : ℕ), ∃ (z : ℤ), (PowerSeries.coeff n) β = ↑z) (u : ℕ) : ∃ (z : ℤ), (PowerSeries.coeff u) (α * β) = ↑z

theorem Biswal.Theorem23.D_coeff_is_int (m a b u : ℕ) : ∃ (z : ℤ), dCoeff ℚ m a b u = ↑z

Transfer matrix decomposition (Steps 2-7 of the proof)

noncomputable def Biswal.Theorem23.stripMatrix (m : ℕ) : Matrix (Fin m) (Fin m) (PowerSeries ℚ)

The tridiagonal transfer matrix with 1 on the diagonal, -1 on the superdiagonal, and -X on the subdiagonal, whose inverse encodes the path counts.

Equations

• Biswal.Theorem23.stripMatrix m i j = if i = j then 1 else if ↑j = ↑i + 1 then -1 else if ↑i = ↑j + 1 then -PowerSeries.X else 0

Helper lemmas for stripMatrix_det

theorem Biswal.Theorem23.stripMatrix_det (m : ℕ) : (stripMatrix m).det = ↑(polyP ℚ m)

Helper lemmas for stripMatrix_inv_entry (minor det and adjugate)

theorem Biswal.Theorem23.stripMatrix_inv_entry (m : ℕ) (hm : 2 ≤ m) (a j : Fin m) (haj : ↑a ≤ ↑j) : (stripMatrix m)⁻¹ a j = ↑(polyP ℚ ↑a * polyP ℚ (m - 1 - ↑j)) * (↑(polyP ℚ m))⁻¹

theorem Biswal.Theorem23.D_coeff_eq_matrix_inv_coeff (m a b u : ℕ) (hm : 2 ≤ m) (ha : a ≤ m - 1) (hb : b ≤ m - 1) (hab : a + b ≤ m - 1) : dCoeff ℚ m a b u = (PowerSeries.coeff u) ((stripMatrix m)⁻¹ ⟨a, ⋯⟩ ⟨m - 1 - b, ⋯⟩)

Helper lemmas for stripMatrix_inv_coeff_nonneg (lattice path)

@[irreducible]

noncomputable def Biswal.Theorem23.pathCount (m : ℕ) (target i : Fin m) (u : ℕ) : ℕ

The number of length-u lattice paths in the Dyck-path model from row i that reach target, used to express the nonnegative coefficients of the matrix inverse.

Equations

• One or more equations did not get rendered due to their size.
• Biswal.Theorem23.pathCount m target i 0 = if ↑i ≤ ↑target then 1 else 0

noncomputable def Biswal.Theorem23.pathCountVec (m : ℕ) (target i : Fin m) : PowerSeries ℚ

The generating power series whose u-th coefficient is pathCount m target i u.

Equations

• Biswal.Theorem23.pathCountVec m target i = PowerSeries.mk fun (u : ℕ) => ↑(Biswal.Theorem23.pathCount m target i u)

theorem Biswal.Theorem23.stripMatrix_inv_coeff_nonneg (m : ℕ) (_hm : 2 ≤ m) (a j : Fin m) (_haj : ↑a ≤ ↑j) (u : ℕ) : 0 ≤ (PowerSeries.coeff u) ((stripMatrix m)⁻¹ a j)

Main theorem

theorem Biswal.Theorem23.thm_manifest_D_nonneg (m a b u : ℕ) (hm : 2 ≤ m) (ha : a ≤ m - 1) (hb : b ≤ m - 1) (hab : a + b ≤ m - 1) : 0 ≤ dCoeff ℚ m a b u

theorem Biswal.Theorem23.D_coeff_eq_nat_cast (m a b u : ℕ) (hm : 2 ≤ m) (ha : a ≤ m - 1) (hb : b ≤ m - 1) (hab : a + b ≤ m - 1) : ∃ (w : ℕ), dCoeff ℚ m a b u = ↑w

Theorem 3: Part (iii) - Nonnegativity of all coefficients

theorem Biswal.Theorem23.thm_manifest_coeff_nonneg (m μ : ℕ) {s : ℕ} (ξ : s.Partition) (hm : 2 ≤ m) (h_parts : ∀ i ∈ ξ.parts, i ≤ m) (hk_nonneg : countMaxParts m ξ ≤ μ / m + 1) (k : ℕ) (hk_eq : k = reducedK m μ ξ) (pairs : Fin k → ℕ × ℕ) (h_bound : ∀ (ν : Fin k), (pairs ν).1 ≤ m - 1 ∧ (pairs ν).2 ≤ m - 1 ∧ (pairs ν).1 + (pairs ν).2 ≤ m - 1) (h_factor : alphaProd ℚ m μ ξ = ∏ ν : Fin k, polyP ℚ (pairs ν).1 * polyP ℚ (pairs ν).2) (r : ℕ) : 0 ≤ genFunCoeff ℚ m μ r ξ