Polynomial multiplication commutes with canonical E-series evaluation

Proved

ArithmeticE.polynomial_mul_series_value

by shivm · Sep 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysise-functionspower-series

Let $f$ be a formal complex power series whose rational factorial-normalized coefficients satisfy the E-function exponential size and common-denominator bounds. For every complex polynomial $P$ and every $z\in\mathbb C$ , canonical series evaluation obeys

\operatorname{value}(Pf,z)=P(z)\operatorname{value}(f,z).

This identifies the formal polynomial products used in scalar differential equations with their analytic values. The proof uses absolute convergence of the E-series, the finite support of the polynomial, and the Cauchy product formula. It needs no value-lifting or arithmetic zero theorem.

Preamble

import Definitions.Def_rationalEArithmetic
open ArithmeticE

Formal statement

theorem ArithmeticE.polynomial_mul_series_value (P : Polynomial ℂ) (f : PowerSeries ℂ)
    (hf : RationalSeriesArithmetic f) (z : ℂ) :
    seriesValue ((P : PowerSeries ℂ)*f) z = P.eval z * seriesValue f z := by sorry

Source

Cauchy product theorem for absolutely convergent series; analytic identification needed in Beukers, https://webspace.science.uu.nl/~beuke106/siegelshidlovskii.pdf, Theorem 3.2.

View graph