E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ≥0
c : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c ↑R)
hd : ∀ (z : ℂ), z ∈ ball c ↑R \ s → DifferentiableAt ℂ f z
hR : 0 < R
w : ℂ
hw : w ∈ EMetric.ball 0 ↑R
hw' : c + w ∈ ball c ↑R
⊢ HasSum (fun n => ↑(cauchyPowerSeries f c (↑R) n) fun x => w) (f (c + w))
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ≥0
c : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c ↑R)
hd : ∀ (z : ℂ), z ∈ ball c ↑R \ s → DifferentiableAt ℂ f z
hR : 0 < R
w : ℂ
hw : w ∈ EMetric.ball 0 ↑R
⊢ HasSum (fun n => ↑(cauchyPowerSeries f c (↑R) n) fun x => w) (f (c + w))
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, ENNReal.coe_lt_coe] using hw
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ≥0
c : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c ↑R)
hd : ∀ (z : ℂ), z ∈ ball c ↑R \ s → DifferentiableAt ℂ f z
hR : 0 < R
w : ℂ
hw : w ∈ EMetric.ball 0 ↑R
hw' : c + w ∈ ball c ↑R
⊢ HasSum (fun n => ↑(cauchyPowerSeries f c (↑R) n) fun x => w)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - (c + w))⁻¹ • f z)
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ≥0
c : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c ↑R)
hd : ∀ (z : ℂ), z ∈ ball c ↑R \ s → DifferentiableAt ℂ f z
hR : 0 < R
w : ℂ
hw : w ∈ EMetric.ball 0 ↑R
hw' : c + w ∈ ball c ↑R
⊢ HasSum (fun n => ↑(cauchyPowerSeries f c (↑R) n) fun x => w) (f (c + w))
rw [← two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
  hs hw' hc hd]
no goals
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ≥0
c : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c ↑R)
hd : ∀ (z : ℂ), z ∈ ball c ↑R \ s → DifferentiableAt ℂ f z
hR : 0 < R
w : ℂ
hw : w ∈ EMetric.ball 0 ↑R
hw' : c + w ∈ ball c ↑R
⊢ HasSum (fun n => ↑(cauchyPowerSeries f c (↑R) n) fun x => w)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - (c + w))⁻¹ • f z)
exact (hasFPowerSeriesOn_cauchy_integral
  ((hc.mono sphere_subset_closedBall).circleIntegrable R.2) hR).hasSum hw
no goals
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ≥0
c : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c ↑R)
hd : ∀ (z : ℂ), z ∈ ball c ↑R \ s → DifferentiableAt ℂ f z
hR : 0 < R
w : ℂ
hw : w ∈ EMetric.ball 0 ↑R
⊢ c + w ∈ ball c ↑R
simpa only [add_mem_ball_iff_norm, ← coe_nnnorm, mem_emetric_ball_zero_iff,
  NNReal.coe_lt_coe, ENNReal.coe_lt_coe] using hw