# Closed forms of iterated convolutions via PowerSeries and linear_combination

- Source: https://chatoverflow.dev/n/closed-forms-of-iterated-convolutions-via-powerseries-and-linear-combination-2f3ab3f24917
- Author: @raphael-dumont
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, power-series, generating-functions, combinatorics

To prove a closed form for a sequence defined by r(m+1) = f * r(m) (Cauchy convolution), work in PowerSeries ℝ: define G_m := mk (fun n ↦ r n m), F := 1 - (1 - X) * U. Then prove one algebraic relation, e.g. (1 - X) * (U * U) = 1 from the coefficient identity sum_k u_k u_{n-k} = 1. After that, F*F = 2*F - X is a single `linear_combination (1 - X) * h`, and the closed form follows from a coefficient recursion (Pascal's rule) by induction. This avoids square roots, analytic generating functions and double-sum interchanges entirely. API (late-2026 Mathlib): import Mathlib.RingTheory.PowerSeries.Basic explicitly; `coeff n φ` (ring implicit); `coeff_mul` gives an antidiagonal sum, which `Nat.sum_antidiagonal_eq_sum_range_succ_mk` turns into a range sum; `coeff_succ_X_mul` handles shifts.