E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
⊢ HasSum (fun n => ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
⊢ HasSum (fun n => ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)
have hR : 0 < R := (Complex.abs.nonneg w).trans_lt hw
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
⊢ HasSum (fun n => ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
⊢ HasSum (fun n => ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)
have hwR : abs w / R ∈ Ico (0 : ℝ) 1 :=
  ⟨div_nonneg (Complex.abs.nonneg w) hR.le, (div_lt_one hR).2 hw⟩
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
n : ℕ
⊢ AEStronglyMeasurable
    (fun θ => deriv (circleMap c R) θ • (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R θ))
    (Measure.restrict volume (Ι 0 (2 * π)))

case refine'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
n : ℕ
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      ‖deriv (circleMap c R) t • (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t)‖ ≤
        (fun n θ => ‖f (circleMap c R θ)‖ * (↑Complex.abs w / R) ^ n) n t

case refine'_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
⊢ ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → Summable fun n => (fun n θ => ‖f (circleMap c R θ)‖ * (↑Complex.abs w / R) ^ n) n t

case refine'_4
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
⊢ IntervalIntegrable (fun t => ∑' (n : ℕ), (fun n θ => ‖f (circleMap c R θ)‖ * (↑Complex.abs w / R) ^ n) n t) volume 0
    (2 * π)

case refine'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      HasSum (fun n => deriv (circleMap c R) t • (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t))
        (deriv (circleMap c R) t • (fun z => (z - (c + w))⁻¹ • f z) (circleMap c R t))
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
⊢ HasSum (fun n => ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)
refine' intervalIntegral.hasSum_integral_of_dominated_convergence
    (fun n θ => ‖f (circleMap c R θ)‖ * (abs w / R) ^ n) (fun n => _) (fun n => _) _ _ _
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
n : ℕ
⊢ AEStronglyMeasurable
    (fun θ => (circleMap 0 R θ * I) • (w / (circleMap c R θ - c)) ^ n • (circleMap c R θ - c)⁻¹ • f (circleMap c R θ))
    (Measure.restrict volume (Ι 0 (2 * π)))
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
n : ℕ
⊢ AEStronglyMeasurable
    (fun θ => deriv (circleMap c R) θ • (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R θ))
    (Measure.restrict volume (Ι 0 (2 * π)))
simp only [deriv_circleMap]
case refine'_1.hf.hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
n : ℕ
⊢ Measurable fun x => circleMap 0 R x * I

case refine'_1.hg.hf.hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
n : ℕ
⊢ Measurable fun x => (w / (circleMap c R x - c)) ^ n

case refine'_1.hg.hg.hf.hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
n : ℕ
⊢ Measurable fun x => (circleMap c R x - c)⁻¹
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
n : ℕ
⊢ AEStronglyMeasurable
    (fun θ => (circleMap 0 R θ * I) • (w / (circleMap c R θ - c)) ^ n • (circleMap c R θ - c)⁻¹ • f (circleMap c R θ))
    (Measure.restrict volume (Ι 0 (2 * π)))
apply_rules [AEStronglyMeasurable.smul, hf.def.1] <;> apply Measurable.aestronglyMeasurable
no goals
case refine'_1.hf.hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
n : ℕ
⊢ Measurable fun x => circleMap 0 R x * I
exact (measurable_circleMap 0 R).mul_const I
no goals
case refine'_1.hg.hf.hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
n : ℕ
⊢ Measurable fun x => (w / (circleMap c R x - c)) ^ n
exact (((measurable_circleMap c R).sub measurable_const).const_div w).pow measurable_const
no goals
case refine'_1.hg.hg.hf.hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
n : ℕ
⊢ Measurable fun x => (circleMap c R x - c)⁻¹
exact ((measurable_circleMap c R).sub measurable_const).inv
no goals
case refine'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
n : ℕ
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      ‖deriv (circleMap c R) t • (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t)‖ ≤
        (fun n θ => ‖f (circleMap c R θ)‖ * (↑Complex.abs w / R) ^ n) n t
simp [norm_smul, abs_of_pos hR, mul_left_comm R, inv_mul_cancel_left₀ hR.ne', mul_comm ‖_‖]
no goals
case refine'_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
⊢ ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → Summable fun n => (fun n θ => ‖f (circleMap c R θ)‖ * (↑Complex.abs w / R) ^ n) n t
exact eventually_of_forall fun _ _ => (summable_geometric_of_lt_1 hwR.1 hwR.2).mul_left _
no goals
case refine'_4
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
⊢ IntervalIntegrable (fun t => ∑' (n : ℕ), (fun n θ => ‖f (circleMap c R θ)‖ * (↑Complex.abs w / R) ^ n) n t) volume 0
    (2 * π)
simpa only [tsum_mul_left, tsum_geometric_of_lt_1 hwR.1 hwR.2] using
  hf.norm.mul_continuousOn continuousOn_const
case refine'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
θ : ℝ
x✝ : θ ∈ Ι 0 (2 * π)
⊢ HasSum (fun n => (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R θ))
    ((fun z => (z - (c + w))⁻¹ • f z) (circleMap c R θ))
case refine'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      HasSum (fun n => deriv (circleMap c R) t • (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t))
        (deriv (circleMap c R) t • (fun z => (z - (c + w))⁻¹ • f z) (circleMap c R t))
refine' eventually_of_forall fun θ _ => HasSum.const_smul _ _
case refine'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
θ : ℝ
x✝ : θ ∈ Ι 0 (2 * π)
⊢ HasSum (fun n => ((w / (circleMap c R θ - c)) ^ n * (circleMap c R θ - c)⁻¹) • f (circleMap c R θ))
    ((circleMap c R θ - (c + w))⁻¹ • f (circleMap c R θ))
case refine'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
θ : ℝ
x✝ : θ ∈ Ι 0 (2 * π)
⊢ HasSum (fun n => (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R θ))
    ((fun z => (z - (c + w))⁻¹ • f z) (circleMap c R θ))
simp only [smul_smul]
case refine'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
θ : ℝ
x✝ : θ ∈ Ι 0 (2 * π)
⊢ HasSum (fun n => (w / (circleMap c R θ - c)) ^ n * (circleMap c R θ - c)⁻¹) (circleMap c R θ - (c + w))⁻¹
case refine'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
θ : ℝ
x✝ : θ ∈ Ι 0 (2 * π)
⊢ HasSum (fun n => ((w / (circleMap c R θ - c)) ^ n * (circleMap c R θ - c)⁻¹) • f (circleMap c R θ))
    ((circleMap c R θ - (c + w))⁻¹ • f (circleMap c R θ))
refine' HasSum.smul_const _ _
case refine'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
θ : ℝ
x✝ : θ ∈ Ι 0 (2 * π)
this : ‖w / (circleMap c R θ - c)‖ < 1
⊢ HasSum (fun n => (w / (circleMap c R θ - c)) ^ n * (circleMap c R θ - c)⁻¹) (circleMap c R θ - (c + w))⁻¹
case refine'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
θ : ℝ
x✝ : θ ∈ Ι 0 (2 * π)
⊢ HasSum (fun n => (w / (circleMap c R θ - c)) ^ n * (circleMap c R θ - c)⁻¹) (circleMap c R θ - (c + w))⁻¹
have : ‖w / (circleMap c R θ - c)‖ < 1 := by simpa [abs_of_pos hR] using hwR.2
case h.e'_6
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
θ : ℝ
x✝ : θ ∈ Ι 0 (2 * π)
this : ‖w / (circleMap c R θ - c)‖ < 1
⊢ (circleMap c R θ - (c + w))⁻¹ = (1 - w / (circleMap c R θ - c))⁻¹ * (circleMap c R θ - c)⁻¹
case refine'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
θ : ℝ
x✝ : θ ∈ Ι 0 (2 * π)
this : ‖w / (circleMap c R θ - c)‖ < 1
⊢ HasSum (fun n => (w / (circleMap c R θ - c)) ^ n * (circleMap c R θ - c)⁻¹) (circleMap c R θ - (c + w))⁻¹
convert (hasSum_geometric_of_norm_lt_1 this).mul_right _ using 1
no goals
case h.e'_6
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
θ : ℝ
x✝ : θ ∈ Ι 0 (2 * π)
this : ‖w / (circleMap c R θ - c)‖ < 1
⊢ (circleMap c R θ - (c + w))⁻¹ = (1 - w / (circleMap c R θ - c))⁻¹ * (circleMap c R θ - c)⁻¹
simp [← sub_sub, ← mul_inv, sub_mul, div_mul_cancel _ (circleMap_ne_center hR.ne')]
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ↑Complex.abs w < R
hR : 0 < R
hwR : ↑Complex.abs w / R ∈ Ico 0 1
θ : ℝ
x✝ : θ ∈ Ι 0 (2 * π)
⊢ ‖w / (circleMap c R θ - c)‖ < 1
simpa [abs_of_pos hR] using hwR.2