Formal logarithms of power series

For a power series f with constant coefficient one, Mathlib's PowerSeries.logOf f is the formal expansion of log f. This file defines its formal derivative and records the characteristic identity

logDeriv f * f = derivative f.

Thus over a field it is the usual quotient f' / f. The multiplicative identity is more general: it needs only a commutative ring over the rationals, because the constant coefficient one makes f - 1 a valid substitution into the logarithm series.

The file also truncates Mathlib's formal identity (log A).subst (exp A - 1) = X to polynomials: composing the truncations of the two series gives X below both truncation degrees. Evaluating these polynomial identities is how the identity log (exp x) = x is proved at points where the two series converge, for instance on the deep ideals of a p-adic field.

Main definitions

• PowerSeries.logDeriv: the formal derivative of PowerSeries.logOf.
• PowerSeries.coeff_logDeriv: the coefficient formula for the formal logarithmic derivative.
• PowerSeries.logDeriv_mul: the product identity characterizing the logarithmic derivative.
• PowerSeries.logDeriv_eq_derivative_mul_inv: the quotient form over a field.
• PowerSeries.coeff_trunc_log_comp_trunc_exp_sub_one: the identity log (exp X) = X, truncated to polynomials: the composite of the truncations of the two series agrees with X below both truncation degrees.

noncomputable def PowerSeries.logDeriv {A : Type u_1} [CommRing A] [Algebra ℚ A] (f : PowerSeries A) : PowerSeries A

The formal logarithmic derivative of a power series: the derivative of PowerSeries.logOf f. When f has constant coefficient one, this is characterized by PowerSeries.logDeriv_mul.

Equations

• f.logDeriv = PowerSeries.derivative f.logOf

theorem PowerSeries.logDeriv_def {A : Type u_1} [CommRing A] [Algebra ℚ A] (f : PowerSeries A) : f.logDeriv = derivative f.logOf

The formal logarithmic derivative is the derivative of the formal logarithm.

theorem PowerSeries.coeff_logDeriv {A : Type u_1} [CommRing A] [Algebra ℚ A] (f : PowerSeries A) (n : ℕ) : (coeff n) f.logDeriv = (coeff (n + 1)) f.logOf * (↑n + 1)

Coefficients of the formal logarithmic derivative are the shifted coefficients of the formal logarithm, multiplied by their positive degree.

theorem PowerSeries.logDeriv_mul {A : Type u_1} [CommRing A] [Algebra ℚ A] (f : PowerSeries A) (hf : constantCoeff f = 1) : f.logDeriv * f = derivative f

The formal logarithmic derivative of a power series with constant coefficient one satisfies (log f)' * f = f'.

theorem PowerSeries.logDeriv_eq_derivative_mul_inv {k : Type u_2} [Field k] [Algebra ℚ k] (f : PowerSeries k) (hf : constantCoeff f = 1) : f.logDeriv = derivative f * f⁻¹

Over a field, the formal logarithmic derivative of a power series with constant coefficient one is the quotient f' / f.

theorem PowerSeries.coeff_trunc_log_comp_trunc_exp_sub_one {A : Type u_1} [CommRing A] [Algebra ℚ A] {M N k : ℕ} (hM : k < M) (hN : k < N) : (((trunc M) (log A)).comp ((trunc N) (exp A - 1))).coeff k = Polynomial.X.coeff k

Below degrees M and N, composing the truncation of the logarithm series below degree M after the truncation of exp - 1 below degree N gives X: this is the truncated form of PowerSeries.subst_log_exp_sub_one. It is what evaluates the identity log (exp x) = x at a point where the two series converge.