Documentation

LeanPool.RegtsSevenster.RS.Classical.SymFun.SuperPowerSums

Super power sums #

The central symmetric-function lemmas for the Regts–Sevenster development. Given a sequence t : ℕ → ℂ whose Schur specialization vanishes outside a hook, t decomposes as a difference of power sums of two disjoint multisets of nonzero complex numbers (Lemma A.9 of the accompanying paper); if t is eventually zero, then t is identically zero from degree 1 onward (Lemma A.10 there).

The key technical ingredient is the identity derivative H = T * H where H is the generating power series of newtonH t and T is the shifted power-sum series; this is immediate from the Newton recursion that defines newtonH.

The generating series and its derivative #

source
noncomputable def RS.newtonHSeries (t : ℕ → ℂ) :
PowerSeries ℂ

The generating power series of the complete homogeneous sequence: H = PowerSeries.mk (newtonH t).

Equations
Instances For
    source
    noncomputable def RS.powerSumSeries (t : ℕ → ℂ) :
    PowerSeries ℂ

    The shifted power-sum series: coefficient n is t (n + 1).

    Equations
    Instances For
      source
      theorem RS.newtonH_derivative (t : ℕ → ℂ) :
      PowerSeries.derivative (newtonHSeries t) = powerSumSeries t * newtonHSeries t

      The derivative identity for the Newton generating series. d⁄dX (newtonHSeries t) = powerSumSeries t * newtonHSeries t, i.e. H' = T · H where H = ∑ h_n X^n and T = ∑ t_{n+1} X^n. This is a direct restatement of the Newton recursion at the level of formal power series.

      source
      @[simp]
      theorem RS.newtonH_series_constantCoeff (t : ℕ → ℂ) :
      PowerSeries.constantCoeff (newtonHSeries t) = 1

      The constant coefficient of newtonHSeries t is 1.

      Power series eventually zero implies polynomial coercion #

      source
      theorem RS.powerSeries_eq_coe_trunc_of_eventually_zero {R : Type u_1} [CommSemiring R] (f : PowerSeries R) (N : ℕ) (hf : ∀ (m : ℕ), N ≤ m → (PowerSeries.coeff m) f = 0) :
      f = ↑((PowerSeries.trunc N) f)

      A power series whose coefficients vanish from degree N onward equals the coercion of its truncation to a polynomial.

      Lemma A.10: eventually zero power sums vanish #

      source
      theorem RS.powerSums_zero_of_eventually_zero {t : ℕ → ℂ} {α β : Multiset ℂ} (hα : ∀ x ∈ α, x ≠ 0) (hβ : ∀ x ∈ β, x ≠ 0) (hdisj : ∀ x ∈ α, x ∉ β) (hps : ∀ (m : ℕ), 1 ≤ m → t m = (Multiset.map (fun (x : ℂ) => x ^ m) α).sum - (Multiset.map (fun (x : ℂ) => x ^ m) β).sum) (hev : ∃ (N₀ : ℕ), ∀ (m : ℕ), N₀ ≤ m → t m = 0) (m : ℕ) :
      1 ≤ m → t m = 0

      Lemma A.10 of the accompanying paper. If t m = ∑ αᵢ^m − ∑ βⱼ^m for all m ≥ 1 with α and β multisets of nonzero complex numbers having disjoint supports, and t is eventually zero, then t m = 0 for all m ≥ 1.

      The proof is direct: the power-sum difference is rewritten as a single weighted exponential sum over the union of supports; vanishing at sufficiently many consecutive exponents forces all weights to be zero by a Vandermonde argument; but disjointness makes every weight nonzero, so the support set must be empty.