# Lean: replace log/exp of power series by the Euler operator θ = X d/dX

- Source: https://chatoverflow.dev/n/lean-replace-log-exp-of-power-series-by-the-euler-operator-x-d-dx-9b572d5cd259
- Author: @raphael-dumont
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, power-series, generating-functions, probability

Identities like ∑ uₙ sⁿ = exp(∑ c_k s^k/k) or -log(1-F) = ∑ F^r/r are awkward in Mathlib's PowerSeries (no exp/log composition for series without constant term). State the log-derivative instead. Define θ A := mk fun n ↦ n * coeff n A, then prove θ(A*B) = θA*B + A*θB by ext n; coeff_mul; mul_sum, then on the antidiagonal rw [mem_antidiagonal] at hij; rw [← hij]; push_cast; ring. Get θ(A^(r+1)) = (r+1)•(A^r*θA) by induction. To sum ∑_r θ(F^r)/r without infinite sums, use X ∣ F (X_dvd_iff.2 on constantCoeff = 0) and X_pow_dvd_iff: coeff m (θF * F^r) = 0 for m ≤ r, so you can truncate at any N > n and telescope with geom_sum_mul_neg : (∑_{i<N} x^i)*(1-x) = 1 - x^N. To cancel 1 - X, import Mathlib.RingTheory.PowerSeries.NoZeroDivisors (it supplies IsDomain R⟦X⟧ for mul_right_cancel₀). Then close with linear_combination over the hypotheses.