Zeta series characterization

The Newton generating series newtonHSeries t is the unique power series with constant term 1 satisfying the trace-zeta differential equation H' = S · H, where S = powerSumSeries t is the shifted power-sum series. This file establishes the ODE-uniqueness principle for formal power series over ℂ and applies it to characterize the Newton series.

ODE uniqueness for formal power series

theorem RS.powerSeries_ode_unique {F G S : PowerSeries ℂ} (hF0 : PowerSeries.constantCoeff F = 1) (hG0 : PowerSeries.constantCoeff G = 1) (hF : PowerSeries.derivative F = S * F) (hG : PowerSeries.derivative G = S * G) : F = G

ODE uniqueness for formal power series over ℂ. If two power series F and G both have constant term 1 and satisfy the same first-order linear ODE F' = S · F, then F = G.

Proof: coefficient induction. The ODE implies (n+1) · coeff (n+1) F = ∑_{i+j=n} coeff i S · coeff j F; since all coefficients up to n agree by the inductive hypothesis, the sums for F and G coincide, and (n+1) ≠ 0 in ℂ allows cancellation.

The Newton ODE

theorem RS.newtonH_series_ode (t : ℕ → ℂ) : PowerSeries.derivative (newtonHSeries t) = powerSumSeries t * newtonHSeries t

The Newton generating series satisfies the trace-zeta ODE: d⁄dX (newtonHSeries t) = powerSumSeries t * newtonHSeries t. This is a re-export of newtonH_derivative.

The zeta characterization

theorem RS.eq_newtonH_series_of_ode {t : ℕ → ℂ} {F : PowerSeries ℂ} (hF0 : PowerSeries.constantCoeff F = 1) (hF : PowerSeries.derivative F = powerSumSeries t * F) : F = newtonHSeries t

Any power series with constant term 1 satisfying the trace-zeta differential equation is the Newton series: the trace zeta function IS the complete homogeneous generating function.