English
If f is differentiable on a closed ball around c and continuous on its boundary, then f has a power series expansion around c that converges on the ball of radius R, with coefficients given by the Cauchy power series.
Русский
Если f дифференцируема на замкнутом шаре вокруг c и непрерывна на границе, то f имеет разложение в степенной ряд вокруг c, сходящийся в шаре радиуса R, коэффициенты задаются через cauchyPowerSeries.
LaTeX
$$HasFPowerSeriesOnBall f (cauchyPowerSeries f c R) c R$$
Lean4
/-- If `f : ℂ → E` is continuous on a closed ball of positive radius and is differentiable at all
but countably many points of the corresponding open ball, then it is analytic on the open ball with
coefficients of the power series given by Cauchy integral formulas. -/
theorem hasFPowerSeriesOnBall_of_differentiable_off_countable {R : ℝ≥0} {c : ℂ} {f : ℂ → E} {s : Set ℂ}
(hs : s.Countable) (hc : ContinuousOn f (closedBall c R)) (hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z)
(hR : 0 < R) : HasFPowerSeriesOnBall f (cauchyPowerSeries f c R) c R
where
r_le := le_radius_cauchyPowerSeries _ _ _
r_pos := ENNReal.coe_pos.2 hR
hasSum := fun {w} hw =>
by
have hw' : c + w ∈ ball c R := by
simpa only [add_mem_ball_iff_norm, ← coe_nnnorm, mem_emetric_ball_zero_iff, NNReal.coe_lt_coe, enorm_lt_coe] using
hw
rw [← two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable hs hw' hc hd]
exact (hasFPowerSeriesOn_cauchy_integral ((hc.mono sphere_subset_closedBall).circleIntegrable R.2) hR).hasSum hw
