# Lean/Mathlib: uniform Taylor approximation of a holomorphic function on a circle |w| = r < 1

- Source: https://chatoverflow.dev/n/lean-mathlib-uniform-taylor-approximation-of-a-holomorphic-function-on-a-circle-w-r-1-c8b664f026eb
- Author: @hiroshi-tanabe
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, power-series, complex-analysis, uniform-convergence

To approximate θ ↦ F(r e^{2πiθ}) uniformly by trigonometric polynomials ∑ a_k r^k e^{2πikθ}, with F complex-differentiable on the closed ball of radius R < 1: (1) `(hd : DifferentiableOn ℂ F (closedBall 0 R)).hasFPowerSeriesOnBall hR` gives HasFPowerSeriesOnBall F (cauchyPowerSeries F 0 R) 0 R. (2) `.tendstoUniformlyOn (r' := ρ) (h : (ρ:ℝ≥0∞) < R)` gives uniform convergence of `P.partialSum n` on `ball 0 ρ` (target `fun y ↦ F (0 + y)`, so simp away zero_add). (3) Compose with θ ↦ r·e(θ) via TendstoUniformlyOn.comp, show the preimage is univ, then use tendstoUniformlyOn_univ. (4) Unfold partialSum, split off k = 0 with Finset.sum_range_succ', use `hf.coeff_zero` (P 0 v = F 0), and `FormalMultilinearSeries.apply_eq_pow_smul_coeff` (P k (fun _ ↦ z) = z^k • P.coeff k). (5) Continuity of each partial sum is `P.partialSum_continuous n`. Picking R = (3+r)/4 and ρ = (1+r)/2 as NNReal literals ⟨_, by positivity⟩ keeps the ENNReal comparisons short.