Evaluating the complete homogeneous symmetric polynomial

The complete homogeneous symmetric polynomial h_d in variables indexed by a finite type σ is the sum of all monomials of degree d, one for each unordered d-tuple of indices. Evaluating it at a family f : σ → R therefore sums, over those unordered tuples, the product of the values f takes on the tuple: TauCeti.eval_hsymm.

In two variables the unordered d-tuples are the d + 1 splittings counted by TauCeti.symFinTwoEquiv, and the evaluation reads h_d(x, y) = ∑_{i ≤ d} xⁱ y^{d-i}: TauCeti.eval_hsymm_fin_two.

Reading the unordered tuples as their multiplicity functions instead writes h_d as the sum of the monomials of degree d, indexed by Finset.piAntidiag: TauCeti.hsymm_eq_sum_piAntidiag. Summed over all degrees, this is the generating function ∑ₙ hₙ tⁿ = ∏ᵢ ∑ₙ xᵢⁿ tⁿ, the product over the variables of the geometric series (1 - xᵢ t)⁻¹: TauCeti.mk_hsymm_eq_prod_mk_pow.

Determinantal formulas such as Jacobi--Trudi index h by integers, h_m being 0 for m < 0; reading a negative index as 0 through a truncated subtraction of natural numbers would silently give the wrong formula. TauCeti.hsymmInt is this integer-indexed complete homogeneous symmetric polynomial.

Main results

• TauCeti.eval_hsymm evaluates the complete homogeneous symmetric polynomial as a sum over the unordered d-tuples of indices.
• TauCeti.eval_hsymm_fin_two reads that off in two variables: h_d(x, y) = ∑_{i ≤ d} xⁱ y^{d-i}.
• TauCeti.hsymm_eq_sum_piAntidiag writes h_d as the sum of the monomials of degree d.
• TauCeti.mk_hsymm_eq_prod_mk_pow: the generating function of the h_d.
• TauCeti.hsymmInt: the complete homogeneous symmetric polynomial h_m of an integer degree m, which is 0 for m < 0.

theorem TauCeti.eval_hsymm {σ : Type u_1} {R : Type u_2} [Fintype σ] [DecidableEq σ] [CommSemiring R] (f : σ → R) (d : ℕ) : (MvPolynomial.eval f) (MvPolynomial.hsymm σ R d) = ∑ s : Sym σ d, (Multiset.map f ↑s).prod

The complete homogeneous symmetric polynomial evaluated: h_d(f) is the sum, over the unordered d-tuples of indices, of the product of the values f takes on the tuple.

theorem TauCeti.eval_hsymm_fin_two {R : Type u_1} [CommSemiring R] (f : Fin 2 → R) (d : ℕ) : (MvPolynomial.eval f) (MvPolynomial.hsymm (Fin 2) R d) = ∑ i ∈ Finset.range (d + 1), f 0 ^ i * f 1 ^ (d - i)

The complete homogeneous symmetric polynomial in two variables: h_d(x, y) is the sum of all d + 1 monomials xⁱ y^{d-i} of degree d.

theorem TauCeti.hsymm_eq_sum_piAntidiag {σ : Type u_1} [Fintype σ] [DecidableEq σ] (R : Type u_2) [CommSemiring R] (d : ℕ) : MvPolynomial.hsymm σ R d = ∑ γ ∈ Finset.univ.piAntidiag d, ∏ i : σ, MvPolynomial.X i ^ γ i

The monomial expansion of the complete homogeneous symmetric polynomial: h_d is the sum of the monomials ∏ᵢ X_i ^ γ_i over the exponent vectors γ of total degree d. This is the multiplicity-function form of MvPolynomial.hsymm, whose summands are indexed by the unordered d-tuples of variables.

theorem TauCeti.mk_hsymm_eq_prod_mk_pow {σ : Type u_1} [Fintype σ] [DecidableEq σ] (R : Type u_2) [CommSemiring R] : (PowerSeries.mk fun (n : ℕ) => MvPolynomial.hsymm σ R n) = ∏ i : σ, PowerSeries.mk fun (n : ℕ) => MvPolynomial.X i ^ n

The generating function of the complete homogeneous symmetric polynomials: ∑ₙ hₙ tⁿ = ∏ᵢ ∑ₙ xᵢⁿ tⁿ, as power series over MvPolynomial σ R. Each factor is the geometric series (1 - xᵢ t)⁻¹, so the coefficient of tⁿ collects one monomial of degree n for every exponent vector.

noncomputable def TauCeti.hsymmInt (σ : Type u_1) [Fintype σ] [DecidableEq σ] (R : Type u_2) [CommSemiring R] (m : ℤ) : MvPolynomial σ R

The complete homogeneous symmetric polynomial of integer degree m: h_m for m ≥ 0 and 0 for m < 0. This is the indexing determinantal formulas such as Jacobi--Trudi use.

Equations

• TauCeti.hsymmInt σ R m = if 0 ≤ m then MvPolynomial.hsymm σ R m.toNat else 0

@[simp]

theorem TauCeti.hsymmInt_of_nonneg {σ : Type u_1} [Fintype σ] [DecidableEq σ] {R : Type u_2} [CommSemiring R] {m : ℤ} (hm : 0 ≤ m) : hsymmInt σ R m = MvPolynomial.hsymm σ R m.toNat

In a nonnegative degree, TauCeti.hsymmInt is MvPolynomial.hsymm.

@[simp]

theorem TauCeti.hsymmInt_of_neg {σ : Type u_1} [Fintype σ] [DecidableEq σ] {R : Type u_2} [CommSemiring R] {m : ℤ} (hm : m < 0) : hsymmInt σ R m = 0

In a negative degree, TauCeti.hsymmInt vanishes.

theorem TauCeti.hsymmInt_natCast {σ : Type u_1} [Fintype σ] [DecidableEq σ] {R : Type u_2} [CommSemiring R] (n : ℕ) : hsymmInt σ R ↑n = MvPolynomial.hsymm σ R n

In a natural-number degree, TauCeti.hsymmInt is MvPolynomial.hsymm.

theorem TauCeti.hsymmInt_zero {σ : Type u_1} [Fintype σ] [DecidableEq σ] {R : Type u_2} [CommSemiring R] : hsymmInt σ R 0 = 1

h_0 = 1.

@[simp]

theorem TauCeti.map_hsymmInt {σ : Type u_1} [Fintype σ] [DecidableEq σ] {R : Type u_2} [CommSemiring R] {S : Type u_3} [CommSemiring S] (m : ℤ) (f : R →+* S) : (MvPolynomial.map f) (hsymmInt σ R m) = hsymmInt σ S m

Changing the coefficients along a ring homomorphism preserves TauCeti.hsymmInt.

@[simp]

theorem TauCeti.rename_hsymmInt {σ : Type u_1} [Fintype σ] [DecidableEq σ] {R : Type u_2} [CommSemiring R] {τ : Type u_3} [Fintype τ] [DecidableEq τ] (m : ℤ) (e : σ ≃ τ) : (MvPolynomial.rename ⇑e) (hsymmInt σ R m) = hsymmInt τ R m

Renaming the variables along a bijection preserves TauCeti.hsymmInt.