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

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.