Documentation

LeanPool.RegtsSevenster.RS.Classical.Deligne.SuperSeries

Super power sums and their generating series #

The power-sum sequence of the super vector space ℂ^{p|q} is superPS p q c = p + (−1)^{c+1} q: p copies of +1 and q copies of −1, the latter weighted by the super sign. The central result of this module is the generating-function identity

`(1 − X)^p · newtonHSeries (superPS p q) = (1 + X)^q`

in ℂ⟦X⟧, proved by showing that both sides satisfy the differential equation (1 + X) · F′ = q · F with constant coefficient 1, whose coefficient recursion pins the coefficients to C(q, n). Coefficient extraction yields binomial evaluations of newtonH (superPS p q) in the pure cases and, for n > q, a linear recurrence of order p — the input for hook-vanishing arguments.

The super power sums #

source
noncomputable def RS.superPS (p q : ℕ) :
ℕ → ℂ

The power sums of the super vector space ℂ^{p|q}: p copies of +1 and q copies of −1 with the super sign, so superPS p q 1 = p + q, superPS p q 2 = p − q, and so on.

Equations
Instances For
    source
    theorem RS.superPS_add (p q r s : ℕ) :
    (fun (c : ℕ) => superPS p q c + superPS r s c) = superPS (p + r) (q + s)

    Super power sums add under direct sums of super vector spaces.

    source
    theorem RS.superPS_mul (p q r s : ℕ) :
    (fun (c : ℕ) => superPS p q c * superPS r s c) = superPS (p * r + q * s) (p * s + q * r)

    Super power sums multiply under tensor products of super vector spaces.

    Binomial coefficients of (1 ± X)^k #

    The differential equation of the super series #

    The generating-function identity #

    source
    theorem RS.newtonHSeries_superPS (p q : ℕ) :
    (1 - PowerSeries.X) ^ p * newtonHSeries (superPS p q) = (1 + PowerSeries.X) ^ q

    The super binomial identity. The generating series of the complete homogeneous sequence of the super power sums superPS p q satisfies (1 − X)^p · H = (1 + X)^q in ℂ⟦X⟧.

    Binomial evaluations #

    source
    theorem RS.newtonH_superPS_zero_p (q n : ℕ) :
    newtonH (superPS 0 q) n = ↑(q.choose n)

    With p = 0 the complete homogeneous values are the binomial coefficients of (1 + X)^q.

    source
    theorem RS.newtonH_superPS_zero_q (p n : ℕ) (hp : 0 < p) :
    newtonH (superPS p 0) n = ↑((p - 1 + n).choose n)

    With q = 0 and p positive the complete homogeneous values are the binomial coefficients of (1 − X)^{−p}.

    The recurrence beyond degree q #

    source
    theorem RS.newtonH_superPS_rec_antidiagonal (p q : ℕ) {n : ℕ} (hn : q < n) :
    ∑ ij ∈ Finset.antidiagonal n, (-1) ^ ij.1 * ↑(p.choose ij.1) * newtonH (superPS p q) ij.2 = 0

    The order-p recurrence beyond degree q, antidiagonal form: for n > q the convolution of the signed binomial row of (1 − X)^p with the complete homogeneous sequence of superPS p q vanishes.