no goals
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‖
simp [cauchyPowerSeries, norm_smul, Real.pi_pos.le]
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
⊢ 0 ≤ (2 * π)⁻¹
simp [Real.pi_pos.le]
no goals
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 * π)⁻¹ * ((Abs.abs R)⁻¹ ^ n * (Abs.abs R * ((Abs.abs R)⁻¹ * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c R x)‖)))
simp [norm_smul, mul_left_comm (|R|)]
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
n : ℕ
⊢ (2 * π)⁻¹ * ((Abs.abs 0)⁻¹ ^ n * (Abs.abs 0 * ((Abs.abs 0)⁻¹ * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c 0 x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c 0 θ)‖) * (Abs.abs 0)⁻¹ ^ n

case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
hR : R ≠ 0
⊢ (2 * π)⁻¹ * ((Abs.abs R)⁻¹ ^ n * (Abs.abs R * ((Abs.abs R)⁻¹ * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c R x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c R θ)‖) * (Abs.abs R)⁻¹ ^ n
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
⊢ (2 * π)⁻¹ * ((Abs.abs R)⁻¹ ^ n * (Abs.abs R * ((Abs.abs R)⁻¹ * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c R x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c R θ)‖) * (Abs.abs R)⁻¹ ^ n
rcases eq_or_ne R 0 with (rfl | hR)
case inl.zero
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
⊢ 0 ≤ (2 * π)⁻¹ * (2 * π * ‖f c‖)
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
n : ℕ
⊢ (2 * π)⁻¹ * ((Abs.abs 0)⁻¹ ^ n * (Abs.abs 0 * ((Abs.abs 0)⁻¹ * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c 0 x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c 0 θ)‖) * (Abs.abs 0)⁻¹ ^ n
cases n <;> simp [-mul_inv_rev]
case inl.zero
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
⊢ 0 ≤ ‖f c‖
case inl.zero
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
⊢ 0 ≤ (2 * π)⁻¹ * (2 * π * ‖f c‖)
rw [← mul_assoc, inv_mul_cancel (Real.two_pi_pos.ne.symm), one_mul]
no goals
case inl.zero
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
⊢ 0 ≤ ‖f c‖
apply norm_nonneg
case inr.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
hR : R ≠ 0
⊢ Abs.abs R ≠ 0
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
hR : R ≠ 0
⊢ (2 * π)⁻¹ * ((Abs.abs R)⁻¹ ^ n * (Abs.abs R * ((Abs.abs R)⁻¹ * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c R x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c R θ)‖) * (Abs.abs R)⁻¹ ^ n
rw [mul_inv_cancel_left₀, mul_assoc, mul_comm ((|R|)⁻¹ ^ n)]
no goals
case inr.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
hR : R ≠ 0
⊢ Abs.abs R ≠ 0
rwa [Ne.def, _root_.abs_eq_zero]