E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
this : ∀ (z : ℂ), z ∈ sphere c R → ‖(z - c) ^ (-2) • f z‖ ≤ C / (R * R)
⊢ ‖deriv f c‖ ≤ C / R
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
⊢ ‖deriv f c‖ ≤ C / R
have : ∀ z ∈ sphere c R, ‖(z - c) ^ (-2 : ℤ) • f z‖ ≤ C / (R * R) :=
  fun z (hz : abs (z - c) = R) => by
  simpa [-mul_inv_rev, norm_smul, hz, zpow_two, ← div_eq_inv_mul] using
    (div_le_div_right (mul_pos hR hR)).2 (hC z hz)
no goals
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
this : ∀ (z : ℂ), z ∈ sphere c R → ‖(z - c) ^ (-2) • f z‖ ≤ C / (R * R)
⊢ ‖deriv f c‖ ≤ C / R
calc
  ‖deriv f c‖ = ‖(2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - c) ^ (-2 : ℤ) • f z‖ :=
    congr_arg norm (deriv_eq_smul_circleIntegral hR hf)
  _ ≤ R * (C / (R * R)) :=
    (circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const hR.le this)
  _ = C / R := by rw [mul_div_left_comm, div_self_mul_self', div_eq_mul_inv]
no goals
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
z : ℂ
hz : ↑abs (z - c) = R
⊢ ‖(z - c) ^ (-2) • f z‖ ≤ C / (R * R)
simpa [-mul_inv_rev, norm_smul, hz, zpow_two, ← div_eq_inv_mul] using
  (div_le_div_right (mul_pos hR hR)).2 (hC z hz)
no goals
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
this : ∀ (z : ℂ), z ∈ sphere c R → ‖(z - c) ^ (-2) • f z‖ ≤ C / (R * R)
⊢ R * (C / (R * R)) = C / R
rw [mul_div_left_comm, div_self_mul_self', div_eq_mul_inv]