Commit 2026-10-13 16:28 af04d418

View on Github →

feat: Liouville theorem for entire functions with polynomial growth (#43888) As a corollary to the classic Liouville theorem, show that entire functions with polynomial growth are themselves polynomials. This material is used in Project VD, formalizing Value Distribution Theory for meromorphic functions on the complex plane. Claude Code was used to create this PR.

Estimated changes

Modified Mathlib/Analysis/Analytic/IsolatedZeros.lean

deleted theorem HasFPowerSeriesAt.has_fpower_series_dslope_fslope

Modified Mathlib/Analysis/Calculus/DSlope.lean

added theorem AnalyticOn.dslope_of_notMem

added theorem AnalyticWithinAt.dslope_of_ne

added theorem HasFPowerSeriesAt.dslope_fslope

Modified Mathlib/Analysis/Complex/Liouville.lean

added theorem Differentiable.exists_eq_polynomial_eval_of_isBigO_pow

added theorem Differentiable.isBigO_pow_iff_exists_eq_polynomial_eval

added theorem Differentiable.isConst_of_isBigO_one

Modified Mathlib/Analysis/Polynomial/Basic.lean

added theorem Polynomial.isBigO_cobounded_pow_natDegree

Modified Mathlib/Logic/Function/Const.lean

added theorem Set.nontrivial_range_iff