[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R θ : ℝ
⊢ circleMap c R (θ + 2 * π) = circleMap c R θ
[PROOFSTEP]
simp [circleMap, add_mul, exp_periodic _]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R θ : ℝ
⊢ circleMap c R θ - c = circleMap 0 R θ
[PROOFSTEP]
simp [circleMap]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
R θ : ℝ
⊢ ↑Complex.abs (circleMap 0 R θ) = |R|
[PROOFSTEP]
simp [circleMap]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R θ : ℝ
⊢ circleMap c R θ ∈ sphere c |R|
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
hR : 0 ≤ R
θ : ℝ
⊢ circleMap c R θ ∈ sphere c R
[PROOFSTEP]
simpa only [_root_.abs_of_nonneg hR] using circleMap_mem_sphere' c R θ
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R θ : ℝ
⊢ ¬circleMap c R θ ∈ ball c R
[PROOFSTEP]
simp [dist_eq, le_abs_self]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
⊢ range (circleMap c R) = c +ᵥ R • range fun θ => exp (↑θ * I)
[PROOFSTEP]
simp only [← image_vadd, ← image_smul, ← range_comp, vadd_eq_add, circleMap, (· ∘ ·), real_smul]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
⊢ (c +ᵥ R • range fun θ => exp (↑θ * I)) = sphere c |R|
[PROOFSTEP]
rw [Complex.range_exp_mul_I, smul_sphere R 0 zero_le_one]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
⊢ c +ᵥ sphere (R • 0) (‖R‖ * 1) = sphere c |R|
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
⊢ circleMap c R '' Ioc 0 (2 * π) = sphere c |R|
[PROOFSTEP]
rw [← range_circleMap, ← (periodic_circleMap c R).image_Ioc Real.two_pi_pos 0, zero_add]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R θ : ℝ
⊢ circleMap c R θ = c ↔ R = 0
[PROOFSTEP]
simp [circleMap, exp_ne_zero]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R θ : ℝ
⊢ HasDerivAt (circleMap c R) (circleMap 0 R θ * I) θ
[PROOFSTEP]
simpa only [mul_assoc, one_mul, ofRealClm_apply, circleMap, ofReal_one, zero_add] using
  (((ofRealClm.hasDerivAt (x := θ)).mul_const I).cexp.const_mul (R : ℂ)).const_add c
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R θ : ℝ
⊢ deriv (circleMap c R) θ = 0 ↔ R = 0
[PROOFSTEP]
simp [I_ne_zero]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R θ : ℝ
⊢ ↑‖deriv (circleMap c R) θ‖₊ ≤ ↑(↑Real.nnabs R)
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
R : ℝ
z w : ℂ
hw : w ∈ ball z R
⊢ Continuous fun θ => (circleMap z R θ - w)⁻¹
[PROOFSTEP]
have : ∀ θ, circleMap z R θ - w ≠ 0 := by
  simp_rw [sub_ne_zero]
  exact fun θ => circleMap_ne_mem_ball hw θ
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
R : ℝ
z w : ℂ
hw : w ∈ ball z R
⊢ ∀ (θ : ℝ), circleMap z R θ - w ≠ 0
[PROOFSTEP]
simp_rw [sub_ne_zero]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
R : ℝ
z w : ℂ
hw : w ∈ ball z R
⊢ ∀ (θ : ℝ), circleMap z R θ ≠ w
[PROOFSTEP]
exact fun θ => circleMap_ne_mem_ball hw θ
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
R : ℝ
z w : ℂ
hw : w ∈ ball z R
this : ∀ (θ : ℝ), circleMap z R θ - w ≠ 0
⊢ Continuous fun θ => (circleMap z R θ - w)⁻¹
[PROOFSTEP]
exact Continuous.inv₀ (by continuity) this
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
R : ℝ
z w : ℂ
hw : w ∈ ball z R
this : ∀ (θ : ℝ), circleMap z R θ - w ≠ 0
⊢ Continuous fun θ => circleMap z R θ - w
[PROOFSTEP]
continuity
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f g : ℂ → E
c : ℂ
R : ℝ
inst✝ : NormedSpace ℂ E
hf : CircleIntegrable f c R
⊢ IntervalIntegrable (fun θ => deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)
[PROOFSTEP]
simp only [CircleIntegrable, deriv_circleMap, intervalIntegrable_iff] at *
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f g : ℂ → E
c : ℂ
R : ℝ
inst✝ : NormedSpace ℂ E
hf : IntegrableOn (fun θ => f (circleMap c R θ)) (Ι 0 (2 * π))
⊢ IntegrableOn (fun θ => (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π))
[PROOFSTEP]
refine' (hf.norm.const_mul |R|).mono' _ _
[GOAL]
case refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f g : ℂ → E
c : ℂ
R : ℝ
inst✝ : NormedSpace ℂ E
hf : IntegrableOn (fun θ => f (circleMap c R θ)) (Ι 0 (2 * π))
⊢ AEStronglyMeasurable (fun θ => (circleMap 0 R θ * I) • f (circleMap c R θ)) (Measure.restrict volume (Ι 0 (2 * π)))
[PROOFSTEP]
exact ((continuous_circleMap _ _).aestronglyMeasurable.mul_const I).smul hf.aestronglyMeasurable
[GOAL]
case refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f g : ℂ → E
c : ℂ
R : ℝ
inst✝ : NormedSpace ℂ E
hf : IntegrableOn (fun θ => f (circleMap c R θ)) (Ι 0 (2 * π))
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ι 0 (2 * π)),
    ‖(circleMap 0 R a * I) • f (circleMap c R a)‖ ≤ |R| * ‖f (circleMap c R a)‖
[PROOFSTEP]
simp [norm_smul]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
c : ℂ
⊢ CircleIntegrable f c 0
[PROOFSTEP]
simp [CircleIntegrable]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ CircleIntegrable f c R ↔ IntervalIntegrable (fun θ => deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)
[PROOFSTEP]
by_cases h₀ : R = 0
[GOAL]
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : R = 0
⊢ CircleIntegrable f c R ↔ IntervalIntegrable (fun θ => deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)
[PROOFSTEP]
simp [h₀, const]
[GOAL]
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : ¬R = 0
⊢ CircleIntegrable f c R ↔ IntervalIntegrable (fun θ => deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)
[PROOFSTEP]
refine' ⟨fun h => h.out, fun h => _⟩
[GOAL]
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : ¬R = 0
h : IntervalIntegrable (fun θ => deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)
⊢ CircleIntegrable f c R
[PROOFSTEP]
simp only [CircleIntegrable, intervalIntegrable_iff, deriv_circleMap] at h ⊢
[GOAL]
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : ¬R = 0
h : IntegrableOn (fun θ => (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π))
⊢ IntegrableOn (fun θ => f (circleMap c R θ)) (Ι 0 (2 * π))
[PROOFSTEP]
refine' (h.norm.const_mul |R|⁻¹).mono' _ _
[GOAL]
case neg.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : ¬R = 0
h : IntegrableOn (fun θ => (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π))
⊢ AEStronglyMeasurable (fun θ => f (circleMap c R θ)) (Measure.restrict volume (Ι 0 (2 * π)))
[PROOFSTEP]
have H : ∀ {θ}, circleMap 0 R θ * I ≠ 0 := fun {θ} => by simp [h₀, I_ne_zero]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : ¬R = 0
h : IntegrableOn (fun θ => (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π))
θ : ℝ
⊢ circleMap 0 R θ * I ≠ 0
[PROOFSTEP]
simp [h₀, I_ne_zero]
[GOAL]
case neg.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : ¬R = 0
h : IntegrableOn (fun θ => (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π))
H : ∀ {θ : ℝ}, circleMap 0 R θ * I ≠ 0
⊢ AEStronglyMeasurable (fun θ => f (circleMap c R θ)) (Measure.restrict volume (Ι 0 (2 * π)))
[PROOFSTEP]
simpa only [inv_smul_smul₀ H] using
  ((continuous_circleMap 0 R).aestronglyMeasurable.mul_const I).aemeasurable.inv.aestronglyMeasurable.smul
    h.aestronglyMeasurable
[GOAL]
case neg.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : ¬R = 0
h : IntegrableOn (fun θ => (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π))
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ι 0 (2 * π)),
    ‖f (circleMap c R a)‖ ≤ |R|⁻¹ * ‖(circleMap 0 R a * I) • f (circleMap c R a)‖
[PROOFSTEP]
simp [norm_smul, h₀]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
⊢ CircleIntegrable (fun z => (z - w) ^ n) c R ↔ R = 0 ∨ 0 ≤ n ∨ ¬w ∈ sphere c |R|
[PROOFSTEP]
constructor
[GOAL]
case mp
E : Type u_1
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
⊢ CircleIntegrable (fun z => (z - w) ^ n) c R → R = 0 ∨ 0 ≤ n ∨ ¬w ∈ sphere c |R|
[PROOFSTEP]
intro h
[GOAL]
case mp
E : Type u_1
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
h : CircleIntegrable (fun z => (z - w) ^ n) c R
⊢ R = 0 ∨ 0 ≤ n ∨ ¬w ∈ sphere c |R|
[PROOFSTEP]
contrapose! h
[GOAL]
case mp
E : Type u_1
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
h : R ≠ 0 ∧ n < 0 ∧ w ∈ sphere c |R|
⊢ ¬CircleIntegrable (fun z => (z - w) ^ n) c R
[PROOFSTEP]
rcases h with ⟨hR, hn, hw⟩
[GOAL]
case mp.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
hw : w ∈ sphere c |R|
⊢ ¬CircleIntegrable (fun z => (z - w) ^ n) c R
[PROOFSTEP]
simp only [circleIntegrable_iff R, deriv_circleMap]
[GOAL]
case mp.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
hw : w ∈ sphere c |R|
⊢ ¬IntervalIntegrable (fun θ => (circleMap 0 R θ * I) • (circleMap c R θ - w) ^ n) volume 0 (2 * π)
[PROOFSTEP]
rw [← image_circleMap_Ioc] at hw
[GOAL]
case mp.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
hw : w ∈ circleMap c R '' Ioc 0 (2 * π)
⊢ ¬IntervalIntegrable (fun θ => (circleMap 0 R θ * I) • (circleMap c R θ - w) ^ n) volume 0 (2 * π)
[PROOFSTEP]
rcases hw with ⟨θ, hθ, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ Ioc 0 (2 * π)
⊢ ¬IntervalIntegrable (fun θ_1 => (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n) volume 0 (2 * π)
[PROOFSTEP]
replace hθ : θ ∈ [[0, 2 * π]]
[GOAL]
case hθ
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ Ioc 0 (2 * π)
⊢ θ ∈ [[0, 2 * π]]
case mp.intro.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
⊢ ¬IntervalIntegrable (fun θ_1 => (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n) volume 0 (2 * π)
[PROOFSTEP]
exact Icc_subset_uIcc (Ioc_subset_Icc_self hθ)
[GOAL]
case mp.intro.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
⊢ ¬IntervalIntegrable (fun θ_1 => (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n) volume 0 (2 * π)
[PROOFSTEP]
refine' not_intervalIntegrable_of_sub_inv_isBigO_punctured _ Real.two_pi_pos.ne hθ
[GOAL]
case mp.intro.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
⊢ (fun x => (x - θ)⁻¹) =O[𝓝[{θ}ᶜ] θ] fun θ_1 => (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n
[PROOFSTEP]
set f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
[GOAL]
case mp.intro.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
⊢ (fun x => (x - θ)⁻¹) =O[𝓝[{θ}ᶜ] θ] fun θ_1 => (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n
[PROOFSTEP]
have : ∀ᶠ θ' in 𝓝[≠] θ, f θ' ∈ ball (0 : ℂ) 1 \ {0} :=
  by
  suffices : ∀ᶠ z in 𝓝[≠] circleMap c R θ, z - circleMap c R θ ∈ ball (0 : ℂ) 1 \ {0}
  exact
    ((differentiable_circleMap c R θ).hasDerivAt.tendsto_punctured_nhds (deriv_circleMap_ne_zero hR)).eventually this
  filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds (ball_mem_nhds _ zero_lt_one)]
  simp_all [dist_eq, sub_eq_zero]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
⊢ ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
[PROOFSTEP]
suffices : ∀ᶠ z in 𝓝[≠] circleMap c R θ, z - circleMap c R θ ∈ ball (0 : ℂ) 1 \ {0}
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (z : ℂ) in 𝓝[{circleMap c R θ}ᶜ] circleMap c R θ, z - circleMap c R θ ∈ ball 0 1 \ {0}
⊢ ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
case this
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
⊢ ∀ᶠ (z : ℂ) in 𝓝[{circleMap c R θ}ᶜ] circleMap c R θ, z - circleMap c R θ ∈ ball 0 1 \ {0}
[PROOFSTEP]
exact ((differentiable_circleMap c R θ).hasDerivAt.tendsto_punctured_nhds (deriv_circleMap_ne_zero hR)).eventually this
[GOAL]
case this
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
⊢ ∀ᶠ (z : ℂ) in 𝓝[{circleMap c R θ}ᶜ] circleMap c R θ, z - circleMap c R θ ∈ ball 0 1 \ {0}
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds (ball_mem_nhds _ zero_lt_one)]
[GOAL]
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
⊢ ∀ (a : ℂ), a ∈ {circleMap c R θ}ᶜ → a ∈ ball (circleMap c R θ) 1 → a - circleMap c R θ ∈ ball 0 1 \ {0}
[PROOFSTEP]
simp_all [dist_eq, sub_eq_zero]
[GOAL]
case mp.intro.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
⊢ (fun x => (x - θ)⁻¹) =O[𝓝[{θ}ᶜ] θ] fun θ_1 => (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n
[PROOFSTEP]
refine'
  (((hasDerivAt_circleMap c R θ).isBigO_sub.mono inf_le_left).inv_rev (this.mono fun θ' h₁ h₂ => absurd h₂ h₁.2)).trans
    _
[GOAL]
case mp.intro.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
⊢ (fun x => (circleMap c R x - circleMap c R θ)⁻¹) =O[𝓝 θ ⊓ 𝓟 {θ}ᶜ] fun θ_1 =>
    (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n
[PROOFSTEP]
refine' IsBigO.of_bound |R|⁻¹ (this.mono fun θ' hθ' => _)
[GOAL]
case mp.intro.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
⊢ ‖(circleMap c R θ' - circleMap c R θ)⁻¹‖ ≤ |R|⁻¹ * ‖(circleMap 0 R θ' * I) • (circleMap c R θ' - circleMap c R θ) ^ n‖
[PROOFSTEP]
set x := abs (f θ')
[GOAL]
case mp.intro.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ↑Complex.abs (f θ')
⊢ ‖(circleMap c R θ' - circleMap c R θ)⁻¹‖ ≤ |R|⁻¹ * ‖(circleMap 0 R θ' * I) • (circleMap c R θ' - circleMap c R θ) ^ n‖
[PROOFSTEP]
suffices x⁻¹ ≤ x ^ n by
  simpa only [inv_mul_cancel_left₀, abs_eq_zero.not.2 hR, norm_eq_abs, map_inv₀, Algebra.id.smul_eq_mul, map_mul,
    abs_circleMap_zero, abs_I, mul_one, abs_zpow, Ne.def, not_false_iff] using this
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this✝ : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ↑Complex.abs (f θ')
this : x⁻¹ ≤ x ^ n
⊢ ‖(circleMap c R θ' - circleMap c R θ)⁻¹‖ ≤ |R|⁻¹ * ‖(circleMap 0 R θ' * I) • (circleMap c R θ' - circleMap c R θ) ^ n‖
[PROOFSTEP]
simpa only [inv_mul_cancel_left₀, abs_eq_zero.not.2 hR, norm_eq_abs, map_inv₀, Algebra.id.smul_eq_mul, map_mul,
  abs_circleMap_zero, abs_I, mul_one, abs_zpow, Ne.def, not_false_iff] using this
[GOAL]
case mp.intro.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ↑Complex.abs (f θ')
⊢ x⁻¹ ≤ x ^ n
[PROOFSTEP]
have : x ∈ Ioo (0 : ℝ) 1 := by simpa [and_comm] using hθ'
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ↑Complex.abs (f θ')
⊢ x ∈ Ioo 0 1
[PROOFSTEP]
simpa [and_comm] using hθ'
[GOAL]
case mp.intro.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this✝ : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ↑Complex.abs (f θ')
this : x ∈ Ioo 0 1
⊢ x⁻¹ ≤ x ^ n
[PROOFSTEP]
rw [← zpow_neg_one]
[GOAL]
case mp.intro.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this✝ : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ↑Complex.abs (f θ')
this : x ∈ Ioo 0 1
⊢ x ^ (-1) ≤ x ^ n
[PROOFSTEP]
refine' (zpow_strictAnti this.1 this.2).le_iff_le.2 (Int.lt_add_one_iff.1 _)
[GOAL]
case mp.intro.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this✝ : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ↑Complex.abs (f θ')
this : x ∈ Ioo 0 1
⊢ n < -1 + 1
[PROOFSTEP]
exact hn
[GOAL]
case mpr
E : Type u_1
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
⊢ R = 0 ∨ 0 ≤ n ∨ ¬w ∈ sphere c |R| → CircleIntegrable (fun z => (z - w) ^ n) c R
[PROOFSTEP]
rintro (rfl | H)
[GOAL]
case mpr.inl
E : Type u_1
inst✝ : NormedAddCommGroup E
c w : ℂ
n : ℤ
⊢ CircleIntegrable (fun z => (z - w) ^ n) c 0
case mpr.inr
E : Type u_1
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
H : 0 ≤ n ∨ ¬w ∈ sphere c |R|
⊢ CircleIntegrable (fun z => (z - w) ^ n) c R
[PROOFSTEP]
exacts [circleIntegrable_zero_radius,
  ((continuousOn_id.sub continuousOn_const).zpow₀ _ fun z hz =>
      H.symm.imp_left fun (hw : w ∉ sphere c |R|) => sub_ne_zero.2 <| ne_of_mem_of_not_mem hz hw).circleIntegrable']
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
⊢ CircleIntegrable (fun z => (z - w)⁻¹) c R ↔ R = 0 ∨ ¬w ∈ sphere c |R|
[PROOFSTEP]
simp only [← zpow_neg_one, circleIntegrable_sub_zpow_iff]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
⊢ R = 0 ∨ False ∨ ¬w ∈ sphere c |R| ↔ R = 0 ∨ ¬w ∈ sphere c |R|
[PROOFSTEP]
norm_num
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
⊢ (∮ (z : ℂ) in C(c, R), f z) = ∫ (θ : ℝ) in Icc 0 (2 * π), deriv (circleMap c R) θ • f (circleMap c R θ)
[PROOFSTEP]
rw [circleIntegral, intervalIntegral.integral_of_le Real.two_pi_pos.le, Measure.restrict_congr_set Ioc_ae_eq_Icc]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
⊢ (∮ (z : ℂ) in C(c, 0), f z) = 0
[PROOFSTEP]
simp [circleIntegral, const]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f g : ℂ → E
c : ℂ
R : ℝ
hR : 0 ≤ R
h : EqOn f g (sphere c R)
θ : ℝ
x✝ : θ ∈ [[0, 2 * π]]
⊢ deriv (circleMap c R) θ • (fun z => f z) (circleMap c R θ) =
    deriv (circleMap c R) θ • (fun z => g z) (circleMap c R θ)
[PROOFSTEP]
simp only [h (circleMap_mem_sphere _ hR _)]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c w : ℂ
R : ℝ
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z) = ∮ (z : ℂ) in C(c, R), f z
[PROOFSTEP]
rcases eq_or_ne R 0 with (rfl | hR)
[GOAL]
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c w : ℂ
⊢ (∮ (z : ℂ) in C(c, 0), (z - w)⁻¹ • (z - w) • f z) = ∮ (z : ℂ) in C(c, 0), f z
[PROOFSTEP]
simp only [integral_radius_zero]
[GOAL]
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c w : ℂ
R : ℝ
hR : R ≠ 0
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z) = ∮ (z : ℂ) in C(c, R), f z
[PROOFSTEP]
have : (circleMap c R ⁻¹' { w }).Countable := (countable_singleton _).preimage_circleMap c hR
[GOAL]
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c w : ℂ
R : ℝ
hR : R ≠ 0
this : Set.Countable (circleMap c R ⁻¹' {w})
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z) = ∮ (z : ℂ) in C(c, R), f z
[PROOFSTEP]
refine' intervalIntegral.integral_congr_ae ((this.ae_not_mem _).mono fun θ hθ _' => _)
[GOAL]
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c w : ℂ
R : ℝ
hR : R ≠ 0
this : Set.Countable (circleMap c R ⁻¹' {w})
θ : ℝ
hθ : ¬θ ∈ circleMap c R ⁻¹' {w}
_' : θ ∈ Ι 0 (2 * π)
⊢ deriv (circleMap c R) θ • (fun z => (z - w)⁻¹ • (z - w) • f z) (circleMap c R θ) =
    deriv (circleMap c R) θ • (fun z => f z) (circleMap c R θ)
[PROOFSTEP]
change circleMap c R θ ≠ w at hθ
[GOAL]
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c w : ℂ
R : ℝ
hR : R ≠ 0
this : Set.Countable (circleMap c R ⁻¹' {w})
θ : ℝ
_' : θ ∈ Ι 0 (2 * π)
hθ : circleMap c R θ ≠ w
⊢ deriv (circleMap c R) θ • (fun z => (z - w)⁻¹ • (z - w) • f z) (circleMap c R θ) =
    deriv (circleMap c R) θ • (fun z => f z) (circleMap c R θ)
[PROOFSTEP]
simp only [inv_smul_smul₀ (sub_ne_zero.2 <| hθ)]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f g : ℂ → E
c : ℂ
R : ℝ
hf : CircleIntegrable f c R
hg : CircleIntegrable g c R
⊢ (∮ (z : ℂ) in C(c, R), f z - g z) = (∮ (z : ℂ) in C(c, R), f z) - ∮ (z : ℂ) in C(c, R), g z
[PROOFSTEP]
simp only [circleIntegral, smul_sub, intervalIntegral.integral_sub hf.out hg.out]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hf : ∀ (z : ℂ), z ∈ sphere c |R| → ‖f z‖ ≤ C
θ : ℝ
x✝ : θ ∈ Ι 0 (2 * π)
⊢ ‖deriv (circleMap c R) θ • f (circleMap c R θ)‖ = |R| * ‖f (circleMap c R θ)‖
[PROOFSTEP]
simp [norm_smul]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hf : ∀ (z : ℂ), z ∈ sphere c |R| → ‖f z‖ ≤ C
⊢ |R| * C * |2 * π - 0| = 2 * π * |R| * C
[PROOFSTEP]
rw [sub_zero, _root_.abs_of_pos Real.two_pi_pos]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hf : ∀ (z : ℂ), z ∈ sphere c |R| → ‖f z‖ ≤ C
⊢ |R| * C * (2 * π) = 2 * π * |R| * C
[PROOFSTEP]
ac_rfl
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
this : |R| = R
⊢ ∀ (z : ℂ), z ∈ sphere c |R| → ‖f z‖ ≤ C
[PROOFSTEP]
rwa [this]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
this : |R| = R
⊢ 2 * π * |R| * C = 2 * π * R * C
[PROOFSTEP]
rw [this]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
⊢ ‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), f z‖ ≤ R * C
[PROOFSTEP]
have : ‖(2 * π * I : ℂ)⁻¹‖ = (2 * π)⁻¹ := by simp [Real.pi_pos.le]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
⊢ ‖(2 * ↑π * I)⁻¹‖ = (2 * π)⁻¹
[PROOFSTEP]
simp [Real.pi_pos.le]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
this : ‖(2 * ↑π * I)⁻¹‖ = (2 * π)⁻¹
⊢ ‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), f z‖ ≤ R * C
[PROOFSTEP]
rw [norm_smul, this, ← div_eq_inv_mul, div_le_iff Real.two_pi_pos, mul_comm (R * C), ← mul_assoc]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
this : ‖(2 * ↑π * I)⁻¹‖ = (2 * π)⁻¹
⊢ ‖∮ (z : ℂ) in C(c, R), f z‖ ≤ 2 * π * R * C
[PROOFSTEP]
exact norm_integral_le_of_norm_le_const hR hf
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
hlt : ∃ z, z ∈ sphere c R ∧ ‖f z‖ < C
⊢ ‖∮ (z : ℂ) in C(c, R), f z‖ < 2 * π * R * C
[PROOFSTEP]
rw [← _root_.abs_of_pos hR, ← image_circleMap_Ioc] at hlt
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
hlt : ∃ z, z ∈ circleMap c R '' Ioc 0 (2 * π) ∧ ‖f z‖ < C
⊢ ‖∮ (z : ℂ) in C(c, R), f z‖ < 2 * π * R * C
[PROOFSTEP]
rcases hlt with ⟨_, ⟨θ₀, hmem, rfl⟩, hlt⟩
[GOAL]
case intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ ‖∮ (z : ℂ) in C(c, R), f z‖ < 2 * π * R * C
[PROOFSTEP]
calc
  ‖∮ z in C(c, R), f z‖ ≤ ∫ θ in (0)..2 * π, ‖deriv (circleMap c R) θ • f (circleMap c R θ)‖ :=
    intervalIntegral.norm_integral_le_integral_norm Real.two_pi_pos.le
  _ < ∫ _ in (0)..2 * π, R * C :=
    by
    simp only [norm_smul, deriv_circleMap, norm_eq_abs, map_mul, abs_I, mul_one, abs_circleMap_zero, abs_of_pos hR]
    refine'
      intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt Real.two_pi_pos _ continuousOn_const
        (fun θ _ => _) ⟨θ₀, Ioc_subset_Icc_self hmem, _⟩
    ·
      exact
        continuousOn_const.mul
          (hc.comp (continuous_circleMap _ _).continuousOn fun θ _ => circleMap_mem_sphere _ hR.le _).norm
    · exact mul_le_mul_of_nonneg_left (hf _ <| circleMap_mem_sphere _ hR.le _) hR.le
    · exact (mul_lt_mul_left hR).2 hlt
  _ = 2 * π * R * C := by simp [mul_assoc]; ring
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ ∫ (θ : ℝ) in 0 ..2 * π, ‖deriv (circleMap c R) θ • f (circleMap c R θ)‖ < ∫ (x : ℝ) in 0 ..2 * π, R * C
[PROOFSTEP]
simp only [norm_smul, deriv_circleMap, norm_eq_abs, map_mul, abs_I, mul_one, abs_circleMap_zero, abs_of_pos hR]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ ∫ (θ : ℝ) in 0 ..2 * π, R * ‖f (circleMap c R θ)‖ < ∫ (x : ℝ) in 0 ..2 * π, R * C
[PROOFSTEP]
refine'
  intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt Real.two_pi_pos _ continuousOn_const
    (fun θ _ => _) ⟨θ₀, Ioc_subset_Icc_self hmem, _⟩
[GOAL]
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ ContinuousOn (fun θ => R * ‖f (circleMap c R θ)‖) (Icc 0 (2 * π))
[PROOFSTEP]
exact
  continuousOn_const.mul
    (hc.comp (continuous_circleMap _ _).continuousOn fun θ _ => circleMap_mem_sphere _ hR.le _).norm
[GOAL]
case refine'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
θ : ℝ
x✝ : θ ∈ Ioc 0 (2 * π)
⊢ R * ‖f (circleMap c R θ)‖ ≤ R * C
[PROOFSTEP]
exact mul_le_mul_of_nonneg_left (hf _ <| circleMap_mem_sphere _ hR.le _) hR.le
[GOAL]
case refine'_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ R * ‖f (circleMap c R θ₀)‖ < R * C
[PROOFSTEP]
exact (mul_lt_mul_left hR).2 hlt
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ ∫ (x : ℝ) in 0 ..2 * π, R * C = 2 * π * R * C
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ R * (2 * (π * C)) = 2 * (π * (R * C))
[PROOFSTEP]
ring
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
𝕜 : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass 𝕜 ℂ E
a : 𝕜
f : ℂ → E
c : ℂ
R : ℝ
⊢ (∮ (z : ℂ) in C(c, R), a • f z) = a • ∮ (z : ℂ) in C(c, R), f z
[PROOFSTEP]
simp only [circleIntegral, ← smul_comm a (_ : ℂ) (_ : E), intervalIntegral.integral_smul]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → ℂ
a : E
c : ℂ
R : ℝ
⊢ (∮ (z : ℂ) in C(c, R), f z • a) = (∮ (z : ℂ) in C(c, R), f z) • a
[PROOFSTEP]
simp only [circleIntegral, intervalIntegral.integral_smul_const, ← smul_assoc]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
hR : R ≠ 0
⊢ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹) = 2 * ↑π * I
[PROOFSTEP]
simp [circleIntegral, ← div_eq_mul_inv, mul_div_cancel_left _ (circleMap_ne_center hR),
  -- porting note: `simp` didn't need a hint to apply `integral_const` hereintervalIntegral.integral_const I]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ (z : ℂ), z ∈ sphere c |R| → HasDerivWithinAt f (f' z) (sphere c |R|) z
⊢ (∮ (z : ℂ) in C(c, R), f' z) = 0
[PROOFSTEP]
by_cases hi : CircleIntegrable f' c R
[GOAL]
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ (z : ℂ), z ∈ sphere c |R| → HasDerivWithinAt f (f' z) (sphere c |R|) z
hi : CircleIntegrable f' c R
⊢ (∮ (z : ℂ) in C(c, R), f' z) = 0
[PROOFSTEP]
rw [← sub_eq_zero.2 ((periodic_circleMap c R).comp f).eq]
[GOAL]
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ (z : ℂ), z ∈ sphere c |R| → HasDerivWithinAt f (f' z) (sphere c |R|) z
hi : CircleIntegrable f' c R
⊢ (∮ (z : ℂ) in C(c, R), f' z) = (f ∘ circleMap c R) (2 * π) - (f ∘ circleMap c R) 0
[PROOFSTEP]
refine' intervalIntegral.integral_eq_sub_of_hasDerivAt (fun θ _ => _) hi.out
[GOAL]
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ (z : ℂ), z ∈ sphere c |R| → HasDerivWithinAt f (f' z) (sphere c |R|) z
hi : CircleIntegrable f' c R
θ : ℝ
x✝ : θ ∈ [[0, 2 * π]]
⊢ HasDerivAt (f ∘ circleMap c R) (deriv (circleMap c R) θ • (fun z => f' z) (circleMap c R θ)) θ
[PROOFSTEP]
exact
  (h _ (circleMap_mem_sphere' _ _ _)).scomp_hasDerivAt θ (differentiable_circleMap _ _ _).hasDerivAt
    (circleMap_mem_sphere' _ _)
[GOAL]
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ (z : ℂ), z ∈ sphere c |R| → HasDerivWithinAt f (f' z) (sphere c |R|) z
hi : ¬CircleIntegrable f' c R
⊢ (∮ (z : ℂ) in C(c, R), f' z) = 0
[PROOFSTEP]
exact integral_undef hi
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
c w : ℂ
R : ℝ
hn : n < 0
hw : w ∈ sphere c |R|
⊢ (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
[PROOFSTEP]
rcases eq_or_ne R 0 with (rfl | h0)
[GOAL]
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
c w : ℂ
hn : n < 0
hw : w ∈ sphere c |0|
⊢ (∮ (z : ℂ) in C(c, 0), (z - w) ^ n) = 0
[PROOFSTEP]
apply integral_radius_zero
[GOAL]
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
c w : ℂ
R : ℝ
hn : n < 0
hw : w ∈ sphere c |R|
h0 : R ≠ 0
⊢ (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
[PROOFSTEP]
apply integral_undef
[GOAL]
case inr.hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
c w : ℂ
R : ℝ
hn : n < 0
hw : w ∈ sphere c |R|
h0 : R ≠ 0
⊢ ¬CircleIntegrable (fun z => (z - w) ^ n) c R
[PROOFSTEP]
simpa [circleIntegrable_sub_zpow_iff, *, not_or]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
⊢ (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
[PROOFSTEP]
rcases em (w ∈ sphere c |R| ∧ n < -1) with (⟨hw, hn⟩ | H)
[GOAL]
case inl.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn✝ : n ≠ -1
c w : ℂ
R : ℝ
hw : w ∈ sphere c |R|
hn : n < -1
⊢ (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
[PROOFSTEP]
exact integral_sub_zpow_of_undef (hn.trans (by decide)) hw
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn✝ : n ≠ -1
c w : ℂ
R : ℝ
hw : w ∈ sphere c |R|
hn : n < -1
⊢ -1 < 0
[PROOFSTEP]
decide
[GOAL]
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ¬(w ∈ sphere c |R| ∧ n < -1)
⊢ (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
[PROOFSTEP]
push_neg at H
[GOAL]
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
⊢ (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
[PROOFSTEP]
have hd : ∀ z, z ≠ w ∨ -1 ≤ n → HasDerivAt (fun z => (z - w) ^ (n + 1) / (n + 1)) ((z - w) ^ n) z :=
  by
  intro z hne
  convert ((hasDerivAt_zpow (n + 1) _ (hne.imp _ _)).comp z ((hasDerivAt_id z).sub_const w)).div_const _ using 1
  · have hn' : (n + 1 : ℂ) ≠ 0 := by rwa [Ne, ← eq_neg_iff_add_eq_zero, ← Int.cast_one, ← Int.cast_neg, Int.cast_inj]
    simp [mul_assoc, mul_div_cancel_left _ hn']
  exacts [sub_ne_zero.2, neg_le_iff_add_nonneg.1]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
⊢ ∀ (z : ℂ), z ≠ w ∨ -1 ≤ n → HasDerivAt (fun z => (z - w) ^ (n + 1) / (↑n + 1)) ((z - w) ^ n) z
[PROOFSTEP]
intro z hne
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ HasDerivAt (fun z => (z - w) ^ (n + 1) / (↑n + 1)) ((z - w) ^ n) z
[PROOFSTEP]
convert ((hasDerivAt_zpow (n + 1) _ (hne.imp _ _)).comp z ((hasDerivAt_id z).sub_const w)).div_const _ using 1
[GOAL]
case h.e'_7
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ (z - w) ^ n = ↑(n + 1) * (id z - w) ^ (n + 1 - 1) * 1 / (↑n + 1)
[PROOFSTEP]
have hn' : (n + 1 : ℂ) ≠ 0 := by rwa [Ne, ← eq_neg_iff_add_eq_zero, ← Int.cast_one, ← Int.cast_neg, Int.cast_inj]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ ↑n + 1 ≠ 0
[PROOFSTEP]
rwa [Ne, ← eq_neg_iff_add_eq_zero, ← Int.cast_one, ← Int.cast_neg, Int.cast_inj]
[GOAL]
case h.e'_7
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
hn' : ↑n + 1 ≠ 0
⊢ (z - w) ^ n = ↑(n + 1) * (id z - w) ^ (n + 1 - 1) * 1 / (↑n + 1)
[PROOFSTEP]
simp [mul_assoc, mul_div_cancel_left _ hn']
[GOAL]
case convert_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ z ≠ w → id z - w ≠ 0
case convert_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ -1 ≤ n → 0 ≤ n + 1
[PROOFSTEP]
exacts [sub_ne_zero.2, neg_le_iff_add_nonneg.1]
[GOAL]
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
hd : ∀ (z : ℂ), z ≠ w ∨ -1 ≤ n → HasDerivAt (fun z => (z - w) ^ (n + 1) / (↑n + 1)) ((z - w) ^ n) z
⊢ (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
[PROOFSTEP]
refine' integral_eq_zero_of_hasDerivWithinAt' fun z hz => (hd z _).hasDerivWithinAt
[GOAL]
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
hd : ∀ (z : ℂ), z ≠ w ∨ -1 ≤ n → HasDerivAt (fun z => (z - w) ^ (n + 1) / (↑n + 1)) ((z - w) ^ n) z
z : ℂ
hz : z ∈ sphere c |R|
⊢ z ≠ w ∨ -1 ≤ n
[PROOFSTEP]
exact (ne_or_eq z w).imp_right fun (h : z = w) => H <| h ▸ hz
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
w : ℂ
⊢ (↑(cauchyPowerSeries f c R n) fun x => w) = (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z
[PROOFSTEP]
simp only [cauchyPowerSeries, ContinuousMultilinearMap.mkPiField_apply, Fin.prod_const, div_eq_mul_inv, mul_pow,
  mul_smul, circleIntegral.integral_smul]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
w : ℂ
⊢ (w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) =
    (2 * ↑π * I)⁻¹ • w ^ n • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z
[PROOFSTEP]
rw [← smul_comm (w ^ n)]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
⊢ ‖cauchyPowerSeries f c R n‖ = (2 * π)⁻¹ * ‖∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖
[PROOFSTEP]
simp [cauchyPowerSeries, norm_smul, Real.pi_pos.le]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
⊢ 0 ≤ (2 * π)⁻¹
[PROOFSTEP]
simp [Real.pi_pos.le]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
⊢ (2 * π)⁻¹ *
      ∫ (θ : ℝ) in 0 ..2 * π,
        ‖deriv (circleMap c R) θ • (circleMap c R θ - c)⁻¹ ^ n • (circleMap c R θ - c)⁻¹ • f (circleMap c R θ)‖ =
    (2 * π)⁻¹ * (|R|⁻¹ ^ n * (|R| * (|R|⁻¹ * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c R x)‖)))
[PROOFSTEP]
simp [norm_smul, mul_left_comm |R|]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
⊢ (2 * π)⁻¹ * (|R|⁻¹ ^ n * (|R| * (|R|⁻¹ * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c R x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c R θ)‖) * |R|⁻¹ ^ n
[PROOFSTEP]
rcases eq_or_ne R 0 with (rfl | hR)
[GOAL]
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
n : ℕ
⊢ (2 * π)⁻¹ * (|0|⁻¹ ^ n * (|0| * (|0|⁻¹ * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c 0 x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c 0 θ)‖) * |0|⁻¹ ^ n
[PROOFSTEP]
cases n
[GOAL]
case inl.zero
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
⊢ (2 * π)⁻¹ * (|0|⁻¹ ^ Nat.zero * (|0| * (|0|⁻¹ * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c 0 x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c 0 θ)‖) * |0|⁻¹ ^ Nat.zero
[PROOFSTEP]
simp [-mul_inv_rev]
[GOAL]
case inl.succ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
n✝ : ℕ
⊢ (2 * π)⁻¹ * (|0|⁻¹ ^ Nat.succ n✝ * (|0| * (|0|⁻¹ * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c 0 x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c 0 θ)‖) * |0|⁻¹ ^ Nat.succ n✝
[PROOFSTEP]
simp [-mul_inv_rev]
[GOAL]
case inl.zero
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
⊢ 0 ≤ (2 * π)⁻¹ * (2 * π * ‖f c‖)
[PROOFSTEP]
rw [← mul_assoc, inv_mul_cancel (Real.two_pi_pos.ne.symm), one_mul]
[GOAL]
case inl.zero
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
⊢ 0 ≤ ‖f c‖
[PROOFSTEP]
apply norm_nonneg
[GOAL]
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
hR : R ≠ 0
⊢ (2 * π)⁻¹ * (|R|⁻¹ ^ n * (|R| * (|R|⁻¹ * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c R x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c R θ)‖) * |R|⁻¹ ^ n
[PROOFSTEP]
rw [mul_inv_cancel_left₀, mul_assoc, mul_comm (|R|⁻¹ ^ n)]
[GOAL]
case inr.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
hR : R ≠ 0
⊢ |R| ≠ 0
[PROOFSTEP]
rwa [Ne.def, _root_.abs_eq_zero]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ≥0
⊢ ↑R ≤ FormalMultilinearSeries.radius (cauchyPowerSeries f c ↑R)
[PROOFSTEP]
refine'
  (cauchyPowerSeries f c R).le_radius_of_bound ((2 * π)⁻¹ * ∫ θ : ℝ in (0)..2 * π, ‖f (circleMap c R θ)‖) fun n => _
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
⊢ ‖cauchyPowerSeries f c (↑R) n‖ * ↑R ^ n ≤ (2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖
[PROOFSTEP]
refine' (mul_le_mul_of_nonneg_right (norm_cauchyPowerSeries_le _ _ _ _) (pow_nonneg R.coe_nonneg _)).trans _
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
⊢ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖) * |↑R|⁻¹ ^ n * ↑R ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖
[PROOFSTEP]
rw [_root_.abs_of_nonneg R.coe_nonneg]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
⊢ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖) * (↑R)⁻¹ ^ n * ↑R ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖
[PROOFSTEP]
cases' eq_or_ne (R ^ n : ℝ) 0 with hR hR
[GOAL]
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
hR : ↑(R ^ n) = 0
⊢ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖) * (↑R)⁻¹ ^ n * ↑R ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖
[PROOFSTEP]
rw_mod_cast [hR, mul_zero]
[GOAL]
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
hR : R ^ n = 0
⊢ 0 ≤ (2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖
[PROOFSTEP]
exact
  mul_nonneg (inv_nonneg.2 Real.two_pi_pos.le)
    (intervalIntegral.integral_nonneg Real.two_pi_pos.le fun _ _ => norm_nonneg _)
[GOAL]
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
hR : ↑(R ^ n) ≠ 0
⊢ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖) * (↑R)⁻¹ ^ n * ↑R ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖
[PROOFSTEP]
rw [inv_pow]
[GOAL]
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
hR : ↑(R ^ n) ≠ 0
⊢ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖) * (↑R ^ n)⁻¹ * ↑R ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖
[PROOFSTEP]
have : (R : ℝ) ^ n ≠ 0 := by norm_cast at hR ⊢
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
hR : ↑(R ^ n) ≠ 0
⊢ ↑R ^ n ≠ 0
[PROOFSTEP]
norm_cast at hR ⊢
[GOAL]
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
hR : ↑(R ^ n) ≠ 0
this : ↑R ^ n ≠ 0
⊢ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖) * (↑R ^ n)⁻¹ * ↑R ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖
[PROOFSTEP]
rw [inv_mul_cancel_right₀ this]
[GOAL]
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)
[PROOFSTEP]
have hR : 0 < R := (Complex.abs.nonneg w).trans_lt hw
[GOAL]
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)
[PROOFSTEP]
have hwR : abs w / R ∈ Ico (0 : ℝ) 1 := ⟨div_nonneg (Complex.abs.nonneg w) hR.le, (div_lt_one hR).2 hw⟩
[GOAL]
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)
[PROOFSTEP]
refine'
  intervalIntegral.hasSum_integral_of_dominated_convergence (fun n θ => ‖f (circleMap c R θ)‖ * (abs w / R) ^ n)
    (fun n => _) (fun n => _) _ _ _
[GOAL]
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 * π)))
[PROOFSTEP]
simp only [deriv_circleMap]
[GOAL]
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 * π)))
[PROOFSTEP]
apply_rules [AEStronglyMeasurable.smul, hf.def.1]
[GOAL]
case refine'_1.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 : ℕ
⊢ AEStronglyMeasurable (fun x => circleMap 0 R x * I) (Measure.restrict volume (Ι 0 (2 * π)))
[PROOFSTEP]
apply Measurable.aestronglyMeasurable
[GOAL]
case refine'_1.hg.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 : ℕ
⊢ AEStronglyMeasurable (fun x => (w / (circleMap c R x - c)) ^ n) (Measure.restrict volume (Ι 0 (2 * π)))
[PROOFSTEP]
apply Measurable.aestronglyMeasurable
[GOAL]
case refine'_1.hg.hg.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 : ℕ
⊢ AEStronglyMeasurable (fun x => (circleMap c R x - c)⁻¹) (Measure.restrict volume (Ι 0 (2 * π)))
[PROOFSTEP]
apply Measurable.aestronglyMeasurable
[GOAL]
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
[PROOFSTEP]
exact (measurable_circleMap 0 R).mul_const I
[GOAL]
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
[PROOFSTEP]
exact (((measurable_circleMap c R).sub measurable_const).const_div w).pow measurable_const
[GOAL]
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)⁻¹
[PROOFSTEP]
exact ((measurable_circleMap c R).sub measurable_const).inv
[GOAL]
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
[PROOFSTEP]
simp [norm_smul, abs_of_pos hR, mul_left_comm R, inv_mul_cancel_left₀ hR.ne', mul_comm ‖_‖]
[GOAL]
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
[PROOFSTEP]
exact eventually_of_forall fun _ _ => (summable_geometric_of_lt_1 hwR.1 hwR.2).mul_left _
[GOAL]
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 * π)
[PROOFSTEP]
simpa only [tsum_mul_left, tsum_geometric_of_lt_1 hwR.1 hwR.2] using hf.norm.mul_continuousOn continuousOn_const
[GOAL]
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))
[PROOFSTEP]
refine' eventually_of_forall fun θ _ => HasSum.const_smul _ _
[GOAL]
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 θ))
[PROOFSTEP]
simp only [smul_smul]
[GOAL]
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 θ))
[PROOFSTEP]
refine' HasSum.smul_const _ _
[GOAL]
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))⁻¹
[PROOFSTEP]
have : ‖w / (circleMap c R θ - c)‖ < 1 := by simpa [abs_of_pos hR] using hwR.2
[GOAL]
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
[PROOFSTEP]
simpa [abs_of_pos hR] using hwR.2
[GOAL]
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))⁻¹
[PROOFSTEP]
convert (hasSum_geometric_of_norm_lt_1 this).mul_right _ using 1
[GOAL]
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)⁻¹
[PROOFSTEP]
simp [← sub_sub, ← mul_inv, sub_mul, div_mul_cancel _ (circleMap_ne_center hR.ne')]
[GOAL]
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 => ↑(cauchyPowerSeries f c R n) fun x => w)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)
[PROOFSTEP]
simp only [cauchyPowerSeries_apply]
[GOAL]
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 => (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)
[PROOFSTEP]
exact (hasSum_two_pi_I_cauchyPowerSeries_integral hf hw).const_smul _
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ≥0
hf : CircleIntegrable f c ↑R
hR : 0 < R
y✝ : ℂ
hy : y✝ ∈ EMetric.ball 0 ↑R
⊢ HasSum (fun n => ↑(cauchyPowerSeries f c (↑R) n) fun x => y✝)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - (c + y✝))⁻¹ • f z)
[PROOFSTEP]
refine' hasSum_cauchyPowerSeries_integral hf _
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ≥0
hf : CircleIntegrable f c ↑R
hR : 0 < R
y✝ : ℂ
hy : y✝ ∈ EMetric.ball 0 ↑R
⊢ ↑Complex.abs y✝ < ↑R
[PROOFSTEP]
rw [← norm_eq_abs, ← coe_nnnorm, NNReal.coe_lt_coe, ← ENNReal.coe_lt_coe]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ≥0
hf : CircleIntegrable f c ↑R
hR : 0 < R
y✝ : ℂ
hy : y✝ ∈ EMetric.ball 0 ↑R
⊢ ↑‖y✝‖₊ < ↑R
[PROOFSTEP]
exact mem_emetric_ball_zero_iff.1 hy
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
R : ℝ
hw : w ∈ ball c R
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹) = 2 * ↑π * I
[PROOFSTEP]
have hR : 0 < R := dist_nonneg.trans_lt hw
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹) = 2 * ↑π * I
[PROOFSTEP]
suffices H : HasSum (fun n : ℕ => ∮ z in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * π * I)
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹) = 2 * ↑π * I
[PROOFSTEP]
have A : CircleIntegrable (fun _ => (1 : ℂ)) c R := continuousOn_const.circleIntegrable'
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)
A : CircleIntegrable (fun x => 1) c R
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹) = 2 * ↑π * I
[PROOFSTEP]
refine' (H.unique _).symm
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)
A : CircleIntegrable (fun x => 1) c R
⊢ HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (∮ (z : ℂ) in C(c, R), (z - w)⁻¹)
[PROOFSTEP]
simpa only [smul_eq_mul, mul_one, add_sub_cancel'_right] using hasSum_two_pi_I_cauchyPowerSeries_integral A hw
[GOAL]
case H
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
⊢ HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)
[PROOFSTEP]
have H : ∀ n : ℕ, n ≠ 0 → (∮ z in C(c, R), (z - c) ^ (-n - 1 : ℤ)) = 0 := by
  refine' fun n hn => integral_sub_zpow_of_ne _ _ _ _; simpa
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
⊢ ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0
[PROOFSTEP]
refine' fun n hn => integral_sub_zpow_of_ne _ _ _ _
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
n : ℕ
hn : n ≠ 0
⊢ -↑n - 1 ≠ -1
[PROOFSTEP]
simpa
[GOAL]
case H
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0
⊢ HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)
[PROOFSTEP]
have : (∮ z in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * π * I := by simp [hR.ne']
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0
⊢ (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * ↑π * I
[PROOFSTEP]
simp [hR.ne']
[GOAL]
case H
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0
this : (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * ↑π * I
⊢ HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)
[PROOFSTEP]
refine' this ▸ hasSum_single _ fun n hn => _
[GOAL]
case H
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0
this : (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * ↑π * I
n : ℕ
hn : n ≠ 0
⊢ (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) = 0
[PROOFSTEP]
simp only [div_eq_mul_inv, mul_pow, integral_const_mul, mul_assoc]
[GOAL]
case H
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0
this : (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * ↑π * I
n : ℕ
hn : n ≠ 0
⊢ ((w - c) ^ n * ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n * (z - c)⁻¹) = 0
[PROOFSTEP]
rw [(integral_congr hR.le fun z hz => _).trans (H n hn), mul_zero]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0
this : (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * ↑π * I
n : ℕ
hn : n ≠ 0
⊢ ∀ (z : ℂ), z ∈ sphere c R → (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ (-↑n - 1)
[PROOFSTEP]
intro z _
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0
this : (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * ↑π * I
n : ℕ
hn : n ≠ 0
z : ℂ
hz✝ : z ∈ sphere c R
⊢ (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ (-↑n - 1)
[PROOFSTEP]
rw [← pow_succ', ← zpow_ofNat, inv_zpow, ← zpow_neg, Int.ofNat_succ, neg_add, sub_eq_add_neg _ (1 : ℤ)]