Cauchy row tests recover coefficients of a local formal series
ProvedOAI.PiExponent.FinitePeriodCollision.rowTest_eq_coeff_of_hasFPowerSeriesAtirrationality-measurenumber-theoryopenai-pi-exponent-017
If a complex-valued function is differentiable on the closed radius-1/2 disk and has at zero the scalar formal series associated to s, then its normalized radius-1/2 Cauchy row test is the ellth coefficient of s. This removes the Cauchy integral and formal-series uniqueness argument from the parent. An independent proof route is to construct the Cauchy power series on the disk from differentiability, identify its formal multilinear series at zero with the supplied one using HasFPowerSeriesAt.eq_formalMultilinearSeries, and evaluate both series at the ellth index and the constant vector 1. This route works at ell = 0 as well.
Preamble
import Definitions.Def_OAI_PiExponent_FinitePeriodAnalytic import Mathlib.Analysis.Complex.CauchyIntegral
Formal statement
theorem OAI.PiExponent.FinitePeriodCollision.rowTest_eq_coeff_of_hasFPowerSeriesAt
(ell : ℕ) (f : ℂ → ℂ) (s : PowerSeries ℂ)
(hd : DifferentiableOn ℂ f (Metric.closedBall 0 (1 / 2)))
(hp : HasFPowerSeriesAt f
(FormalMultilinearSeries.ofScalars ℂ
(fun n => PowerSeries.coeff n s)) 0) :
rowTest ell f = PowerSeries.coeff ell s := by sorrySource