Power-series logarithm lemmas

This module proves the power-series logarithm additivity and coefficient identities used to transport the Connes-Kreimer Eulerian idempotent calculation to convolution algebras.

theorem PowerSeries.one_add_X_mul_deriv_log {A : Type u_1} [CommRing A] [Algebra ℚ A] : (1 + X) * (derivative A) (log A) = 1

(1+X) · (log(1+X))' = 1: the geometric-series identity behind the derivative of log.

theorem PowerSeries.deriv_log_subst_mul {A : Type u_1} [CommRing A] [Algebra ℚ A] {h : PowerSeries A} (hh : constantCoeff h = 1) : subst (h - 1) ((derivative A) (log A)) * h = 1

The derivative (log(1+X))' substituted at h-1 is the inverse of h (for h with constant term 1): (log A)'.subst (h-1) * h = 1.

theorem PowerSeries.deriv_logOf_mul {A : Type u_1} [CommRing A] [Algebra ℚ A] {h : PowerSeries A} (hh : constantCoeff h = 1) : (derivative A) h.logOf * h = (derivative A) h

The chain-rule form of the derivative of logOf: (logOf h)' · h = h' for h with constant term 1.

theorem PowerSeries.logOf_mul {A : Type u_1} [CommRing A] [Algebra ℚ A] [IsAddTorsionFree A] {f g : PowerSeries A} (hf : constantCoeff f = 1) (hg : constantCoeff g = 1) : (f * g).logOf = f.logOf + g.logOf

Logarithm of a product at the power-series level: logOf (f · g) = logOf f + logOf g for f, g with constant term 1.

@[simp]

theorem PowerSeries.logOf_one {A : Type u_1} [CommRing A] [Algebra ℚ A] [IsAddTorsionFree A] : logOf 1 = 0

logOf 1 = 0.

theorem PowerSeries.logOf_pow {A : Type u_1} [CommRing A] [Algebra ℚ A] [IsAddTorsionFree A] {f : PowerSeries A} (hf : constantCoeff f = 1) (n : ℕ) : (f ^ n).logOf = n • f.logOf

Logarithm of a power: logOf (f ^ n) = n • logOf f for f with constant term 1. This is the eigen-relation engine: at f = id in the convolution algebra, logOf (Ψⁱ) = i · logOf id.

theorem PowerSeries.coeff_pow_eq_zero_of_lt {A : Type u_1} [CommRing A] {g : PowerSeries A} (hg : constantCoeff g = 0) {d m : ℕ} (hmd : m < d) : (coeff m) (g ^ d) = 0

A series with zero constant coefficient has its d-th power vanishing below degree d.

theorem PowerSeries.coeff_logTrunc_pow {A : Type u_1} [CommRing A] [Algebra ℚ A] [IsAddTorsionFree A] (p N m : ℕ) (hm : m ≤ N) : (coeff m) (∑ j ∈ Finset.range (N + 1), (coeff j) (log A) • ((1 + X) ^ p - 1) ^ j) = p • (coeff m) (log A)

Coefficient form of logOf_pow (the eigen-transport core). The degree-≤N truncation of the log series, substituted at (1+X)^p − 1, has m-th coefficient p · cₘ for m ≤ N (cₘ = coeff m (log A)). This is what transports to the convolution algebra (evaluate X ↦ J, the per-degree-nilpotent augmentation) to give the Adams eigen-relation Ψᵖ ∘ e⁽¹⁾ = p · e⁽¹⁾.

theorem PowerSeries.polyPL_coeff {A : Type u_1} [CommRing A] [Algebra ℚ A] [IsAddTorsionFree A] (p N m : ℕ) (hm : m ≤ N) : (∑ j ∈ Finset.range (N + 1), Polynomial.C ((coeff j) (log A)) * ((1 + Polynomial.X) ^ p - 1) ^ j).coeff m = p • (coeff m) (log A)

Polynomial form of coeff_logTrunc_pow (Poly↔PowerSeries bridge). For evaluating at a per-degree-nilpotent ring element, such as the convolution J = id − u∘ε, via Polynomial.eval₂.