The power-series logarithm of a product

For power series f, g with constant coefficient 1 over a ℚ-algebra, logOf (f * g) = logOf f + logOf g and logOf (f ^ n) = n • logOf f, where logOf f = log(1 + X) substituted at f - 1 (Mathlib's PowerSeries.logOf). The proof is by uniqueness of antiderivatives (PowerSeries.derivative.ext): no topology and no exp.

Main results

• PowerSeries.deriv_logOf_mul: (logOf h)' · h = h' for h with constant coefficient 1.
• PowerSeries.logOf_mul: logOf (f * g) = logOf f + logOf g.
• PowerSeries.logOf_one, PowerSeries.logOf_pow: logOf 1 = 0, logOf (f ^ n) = n • logOf f.
• PowerSeries.coeff_logTrunc_pow, PowerSeries.polyPL_coeff: the coefficient form of logOf ((1 + X) ^ p) = p • log(1 + X) for the truncated logarithm, as a power series and as a polynomial. This is the form used for the Adams eigen-relation of the Connes–Kreimer Hopf algebra (Formalizations.RingTheory.HopfAlgebra.ConnesKreimer.Eulerian).

Mathlib has logOf, derivative_log_mul_one_add_X ((log(1 + X))' · (1 + X) = 1, used here) and logOf_exp, but at the pinned commit not the additivity logOf_mul.

References

• C. Marín, How a Tree Forgets Its Order: the Eulerian idempotent and the Adams spectrum on the commutative Connes–Kreimer–Butcher Hopf algebra of rooted trees, machine-checked in Lean 4 (2026), doi:10.5281/zenodo.20774821. Ported from PowerSeriesLogMul.lean of karlesmarin/connes-kreimer-lean (Lean v4.30.0-rc2).

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 (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 h.logOf * h = derivative 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] [HasUniqueDiv 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] [HasUniqueDiv A] : logOf 1 = 0

logOf 1 = 0.

theorem PowerSeries.logOf_pow {A : Type u_1} [CommRing A] [Algebra ℚ A] [HasUniqueDiv 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.

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] [HasUniqueDiv 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 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)).

theorem PowerSeries.polyPL_coeff {A : Type u_1} [CommRing A] [Algebra ℚ A] [HasUniqueDiv 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, for evaluation at a ring element through Polynomial.eval₂.