The period function has its formal Taylor series at zero
ProvedOAI.PiExponent.FinitePeriodCollision.hasFPowerSeriesAt_periodFunctionirrationality-measurenumber-theoryopenai-pi-exponent-017
For arbitrary complex b and center and natural h and d, the indicated period function has at zero the formal multilinear series whose scalar coefficients are those of the displayed PowerSeries product. This isolates the logarithm series and formal-series multiplication and power calculations from the Cauchy coefficient step. The independent proof route in the pinned upstream source is to establish HasSum for the coefficients of constants, X, and the formal logarithm on ‖t‖ < 1, combine these with the coefficient-series product and power lemmas, and convert the resulting local HasSum statement to HasFPowerSeriesAt. The zero exponents require no extra hypotheses: the corresponding formal powers are the unit series.
Preamble
import Definitions.Def_OAI_PiExponent_FinitePeriodAnalytic import Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Formal statement
theorem OAI.PiExponent.FinitePeriodCollision.hasFPowerSeriesAt_periodFunction
(b center : ℂ) (h d : ℕ) :
HasFPowerSeriesAt
(fun t : ℂ => b * (1 + t) ^ h * (center + Complex.log (1 + t)) ^ d)
(FormalMultilinearSeries.ofScalars ℂ (fun n =>
PowerSeries.coeff n
(PowerSeries.C b * (1 + PowerSeries.X) ^ h *
(PowerSeries.C center + PowerSeries.log ℂ) ^ d))) 0 := by sorrySource