The trace zeta function in exponential form

traceZeta t = exp (∑_{m≥1} t m / m · zᵐ) as a formal power series, and its identification with the Newton generating series via the differential characterization — the displayed form of the trace zeta function.

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

The power-sum logarithm ∑_{m≥1} t m / m · zᵐ.

Equations

• RS.psLog t = PowerSeries.mk fun (m : ℕ) => if m = 0 then 0 else t m / ↑m

theorem RS.constantCoeff_psLog (t : ℕ → ℂ) : PowerSeries.constantCoeff (psLog t) = 0

The log series has no constant term.

theorem RS.hasSubst_psLog (t : ℕ → ℂ) : PowerSeries.HasSubst (psLog t)

Hence it can be substituted into the exponential.

theorem RS.derivative_psLog (t : ℕ → ℂ) : PowerSeries.derivative (psLog t) = powerSumSeries t

The derivative of the power-sum logarithm is the power-sum series.

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

The trace zeta function in exponential form.

Equations

• RS.traceZeta t = PowerSeries.subst (RS.psLog t) (PowerSeries.exp ℂ)

theorem RS.traceZeta_eq_newtonH_series (t : ℕ → ℂ) : traceZeta t = newtonHSeries t

The zeta identification: the exponential form equals the Newton generating series.