Convolution of complete homogeneous sequences

The complete homogeneous sequence of a sum of scalar sequences is the convolution of the individual sequences: at the level of generating series, newtonHSeries (t + t') = newtonHSeries t * newtonHSeries t'.

The proof follows the house technique: both sides satisfy the first-order differential equation F′ = (T + T′) · F — the left by the Newton derivative identity applied to the sum, the right by the Leibniz rule and the identity applied twice — and both have constant coefficient 1, so they agree by the coefficient recursion that the equation pins down. A reusable uniqueness lemma odeUnique_of_constEq packages the recursion argument.

Coefficient extraction yields the consumer-facing convolution formula newtonH_add, together with its integer-indexed form newtonHZ_add for Jacobi–Trudi consumers.

Additivity of the power-sum series

theorem RS.powerSumSeries_add (t t' : ℕ → ℂ) : (powerSumSeries fun (c : ℕ) => t c + t' c) = powerSumSeries t + powerSumSeries t'

The shifted power-sum series is additive in the scalar sequence.

Uniqueness for the first-order linear ODE

theorem RS.odeUnique_of_constEq (P F G : PowerSeries ℂ) (hF : PowerSeries.derivative F = P * F) (hG : PowerSeries.derivative G = P * G) (h0 : PowerSeries.constantCoeff F = PowerSeries.constantCoeff G) : F = G

Uniqueness for F′ = P · F. Two power series satisfying the same first-order linear differential equation with equal constant coefficients are equal: the equation determines each coefficient from the earlier ones by the recursion (n + 1) · F_{n+1} = ∑_{i+j=n} P_i · F_j, and division by the nonzero scalar n + 1 closes the strong induction.

The convolution identity

theorem RS.newtonHSeries_add (t t' : ℕ → ℂ) : (newtonHSeries fun (c : ℕ) => t c + t' c) = newtonHSeries t * newtonHSeries t'

Convolution of Newton generating series. The generating series of the complete homogeneous sequence of a sum of scalar sequences is the product of the individual generating series.

theorem RS.newtonH_add (t t' : ℕ → ℂ) (n : ℕ) : newtonH (fun (c : ℕ) => t c + t' c) n = ∑ ij ∈ Finset.antidiagonal n, newtonH t ij.1 * newtonH t' ij.2

The convolution formula for complete homogeneous values. h_n (t + t') = ∑_{i+j=n} h_i (t) · h_j (t').

theorem RS.newtonHZ_add (t t' : ℕ → ℂ) (m : ℤ) (hm : 0 ≤ m) : newtonHZ (fun (c : ℕ) => t c + t' c) m = ∑ ij ∈ Finset.antidiagonal m.toNat, newtonHZ t ↑ij.1 * newtonHZ t' ↑ij.2

The convolution formula in the integer-indexed form used by Jacobi–Trudi consumers: for 0 ≤ m the value newtonHZ (t + t') m is the antidiagonal convolution over m.toNat (in negative degrees both sides vanish by newtonHZ_neg, so the nonnegative case carries all content).