Theorem: cauchy2_hasSum_n1n0_bound (Ray/Hartogs/Osgood.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
n : ℕ
z0 : ℂ
z0s : z0 ∈ sphere c0 r
⊢ ‖w1 ^ n • (2 * ↑π * I)⁻¹ • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤
    (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 / r) ^ n
Tactic:
have isb := cauchy1_bound h.rp
  (ContinuousOn.mono (h.fc1 (mem_sphere_closed z0s)) Metric.sphere_subset_closedBall)
  (fun z1 z1s ↦ h.fb z0s z1s) n
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
n : ℕ
z0 : ℂ
z0s : z0 ∈ sphere c0 r
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
⊢ ‖w1 ^ n • (2 * ↑π * I)⁻¹ • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤
    (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 / r) ^ n

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
n : ℕ
z0 : ℂ
z0s : z0 ∈ sphere c0 r
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
⊢ ‖w1 ^ n • (2 * ↑π * I)⁻¹ • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤
    (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 / r) ^ n
Tactic:
simp only [mem_sphere_iff_norm, Complex.norm_eq_abs, Metric.mem_ball, dist_zero_right] at z0s w0m
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
⊢ ‖w1 ^ n • (2 * ↑π * I)⁻¹ • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤
    (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 / r) ^ n

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
⊢ ‖w1 ^ n • (2 * ↑π * I)⁻¹ • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤
    (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 / r) ^ n
Tactic:
have zcw : abs (z0 - (c0 + w0)) ≥ r - abs w0 := by
  calc abs (z0 - (c0 + w0))
    _ = abs (z0 - c0 + -w0) := by ring_nf
    _ ≥ abs (z0 - c0) - abs (-w0) := by bound
    _ = r - abs w0 := by rw [z0s]; simp only [map_neg_eq_map]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
zcw : Complex.abs (z0 - (c0 + w0)) ≥ r - Complex.abs w0
⊢ ‖w1 ^ n • (2 * ↑π * I)⁻¹ • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤
    (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 / r) ^ n

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
zcw : Complex.abs (z0 - (c0 + w0)) ≥ r - Complex.abs w0
⊢ ‖w1 ^ n • (2 * ↑π * I)⁻¹ • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤
    (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 / r) ^ n
Tactic:
have zcw' : (abs (z0 - (c0 + w0)))⁻¹ ≤ (r - abs w0)⁻¹ := by bound
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
zcw : Complex.abs (z0 - (c0 + w0)) ≥ r - Complex.abs w0
zcw' : (Complex.abs (z0 - (c0 + w0)))⁻¹ ≤ (r - Complex.abs w0)⁻¹
⊢ ‖w1 ^ n • (2 * ↑π * I)⁻¹ • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤
    (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 / r) ^ n

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
zcw : Complex.abs (z0 - (c0 + w0)) ≥ r - Complex.abs w0
zcw' : (Complex.abs (z0 - (c0 + w0)))⁻¹ ≤ (r - Complex.abs w0)⁻¹
⊢ ‖w1 ^ n • (2 * ↑π * I)⁻¹ • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤
    (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 / r) ^ n
Tactic:
have a : (abs (2 * π * I : ℂ))⁻¹ = (2 * π)⁻¹ := by
  simp only [map_mul, Complex.abs_two, Complex.abs_ofReal, Complex.abs_I, mul_one, mul_inv_rev,
    mul_eq_mul_right_iff, inv_inj, abs_eq_self, inv_eq_zero, OfNat.ofNat_ne_zero, or_false]
  bound
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
zcw : Complex.abs (z0 - (c0 + w0)) ≥ r - Complex.abs w0
zcw' : (Complex.abs (z0 - (c0 + w0)))⁻¹ ≤ (r - Complex.abs w0)⁻¹
a : (Complex.abs (2 * ↑π * I))⁻¹ = (2 * π)⁻¹
⊢ ‖w1 ^ n • (2 * ↑π * I)⁻¹ • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤
    (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 / r) ^ n

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
zcw : Complex.abs (z0 - (c0 + w0)) ≥ r - Complex.abs w0
zcw' : (Complex.abs (z0 - (c0 + w0)))⁻¹ ≤ (r - Complex.abs w0)⁻¹
a : (Complex.abs (2 * ↑π * I))⁻¹ = (2 * π)⁻¹
⊢ ‖w1 ^ n • (2 * ↑π * I)⁻¹ • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤
    (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 / r) ^ n
Tactic:
rw [norm_smul, norm_smul, norm_smul, Complex.norm_eq_abs, Complex.norm_eq_abs,
  Complex.norm_eq_abs, Complex.abs.map_pow, map_inv₀, map_inv₀, a]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
zcw : Complex.abs (z0 - (c0 + w0)) ≥ r - Complex.abs w0
zcw' : (Complex.abs (z0 - (c0 + w0)))⁻¹ ≤ (r - Complex.abs w0)⁻¹
a : (Complex.abs (2 * ↑π * I))⁻¹ = (2 * π)⁻¹
⊢ Complex.abs w1 ^ n *
      ((2 * π)⁻¹ *
        ((Complex.abs (z0 - (c0 + w0)))⁻¹ * ‖∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1)‖)) ≤
    (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 / r) ^ n

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
zcw : Complex.abs (z0 - (c0 + w0)) ≥ r - Complex.abs w0
zcw' : (Complex.abs (z0 - (c0 + w0)))⁻¹ ≤ (r - Complex.abs w0)⁻¹
a : (Complex.abs (2 * ↑π * I))⁻¹ = (2 * π)⁻¹
⊢ Complex.abs w1 ^ n *
      ((2 * π)⁻¹ *
        ((Complex.abs (z0 - (c0 + w0)))⁻¹ * ‖∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1)‖)) ≤
    (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 / r) ^ n
Tactic:
calc abs w1 ^ n * ((2*π)⁻¹ * ((abs (z0 - (c0 + w0)))⁻¹ *
    ‖∮ z1 in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1)‖))
  _ ≤ abs w1 ^ n * ((2 * π)⁻¹ * ((abs (z0 - (c0 + w0)))⁻¹ * (2 * π * b * r⁻¹ ^ n))) := by bound
  _ ≤ abs w1 ^ n * ((2 * π)⁻¹ * ((r - abs w0)⁻¹ * (2 * π * b * r⁻¹ ^ n))) := by bound
  _ = 2 * π * (2 * π)⁻¹ * (r - abs w0)⁻¹ * b * (abs w1 ^ n * r⁻¹ ^ n) := by ring
  _ = (r - abs w0)⁻¹ * b * (abs w1 / r) ^ n := by
    rw [mul_inv_cancel Real.two_pi_pos.ne', ← mul_pow, ← div_eq_mul_inv _ r, one_mul]
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
⊢ Complex.abs (z0 - (c0 + w0)) ≥ r - Complex.abs w0
Tactic:
calc abs (z0 - (c0 + w0))
  _ = abs (z0 - c0 + -w0) := by ring_nf
  _ ≥ abs (z0 - c0) - abs (-w0) := by bound
  _ = r - abs w0 := by rw [z0s]; simp only [map_neg_eq_map]
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
⊢ Complex.abs (z0 - (c0 + w0)) = Complex.abs (z0 - c0 + -w0)
Tactic:
ring_nf
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
⊢ Complex.abs (z0 - c0 + -w0) ≥ Complex.abs (z0 - c0) - Complex.abs (-w0)
Tactic:
bound
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
⊢ Complex.abs (z0 - c0) - Complex.abs (-w0) = r - Complex.abs w0
Tactic:
rw [z0s]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
⊢ r - Complex.abs (-w0) = r - Complex.abs w0

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
⊢ r - Complex.abs (-w0) = r - Complex.abs w0
Tactic:
simp only [map_neg_eq_map]
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
zcw : Complex.abs (z0 - (c0 + w0)) ≥ r - Complex.abs w0
⊢ (Complex.abs (z0 - (c0 + w0)))⁻¹ ≤ (r - Complex.abs w0)⁻¹
Tactic:
bound
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
zcw : Complex.abs (z0 - (c0 + w0)) ≥ r - Complex.abs w0
zcw' : (Complex.abs (z0 - (c0 + w0)))⁻¹ ≤ (r - Complex.abs w0)⁻¹
⊢ (Complex.abs (2 * ↑π * I))⁻¹ = (2 * π)⁻¹
Tactic:
simp only [map_mul, Complex.abs_two, Complex.abs_ofReal, Complex.abs_I, mul_one, mul_inv_rev,
  mul_eq_mul_right_iff, inv_inj, abs_eq_self, inv_eq_zero, OfNat.ofNat_ne_zero, or_false]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
zcw : Complex.abs (z0 - (c0 + w0)) ≥ r - Complex.abs w0
zcw' : (Complex.abs (z0 - (c0 + w0)))⁻¹ ≤ (r - Complex.abs w0)⁻¹
⊢ 0 ≤ π

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
zcw : Complex.abs (z0 - (c0 + w0)) ≥ r - Complex.abs w0
zcw' : (Complex.abs (z0 - (c0 + w0)))⁻¹ ≤ (r - Complex.abs w0)⁻¹
⊢ 0 ≤ π
Tactic:
bound
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
zcw : Complex.abs (z0 - (c0 + w0)) ≥ r - Complex.abs w0
zcw' : (Complex.abs (z0 - (c0 + w0)))⁻¹ ≤ (r - Complex.abs w0)⁻¹
a : (Complex.abs (2 * ↑π * I))⁻¹ = (2 * π)⁻¹
⊢ Complex.abs w1 ^ n *
      ((2 * π)⁻¹ *
        ((Complex.abs (z0 - (c0 + w0)))⁻¹ * ‖∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1)‖)) ≤
    Complex.abs w1 ^ n * ((2 * π)⁻¹ * ((Complex.abs (z0 - (c0 + w0)))⁻¹ * (2 * π * b * r⁻¹ ^ n)))
Tactic:
bound
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
zcw : Complex.abs (z0 - (c0 + w0)) ≥ r - Complex.abs w0
zcw' : (Complex.abs (z0 - (c0 + w0)))⁻¹ ≤ (r - Complex.abs w0)⁻¹
a : (Complex.abs (2 * ↑π * I))⁻¹ = (2 * π)⁻¹
⊢ Complex.abs w1 ^ n * ((2 * π)⁻¹ * ((Complex.abs (z0 - (c0 + w0)))⁻¹ * (2 * π * b * r⁻¹ ^ n))) ≤
    Complex.abs w1 ^ n * ((2 * π)⁻¹ * ((r - Complex.abs w0)⁻¹ * (2 * π * b * r⁻¹ ^ n)))
Tactic:
bound
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
zcw : Complex.abs (z0 - (c0 + w0)) ≥ r - Complex.abs w0
zcw' : (Complex.abs (z0 - (c0 + w0)))⁻¹ ≤ (r - Complex.abs w0)⁻¹
a : (Complex.abs (2 * ↑π * I))⁻¹ = (2 * π)⁻¹
⊢ Complex.abs w1 ^ n * ((2 * π)⁻¹ * ((r - Complex.abs w0)⁻¹ * (2 * π * b * r⁻¹ ^ n))) =
    2 * π * (2 * π)⁻¹ * (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 ^ n * r⁻¹ ^ n)
Tactic:
ring
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n : ℕ
z0 : ℂ
isb : ‖∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z)‖ ≤ 2 * π * b * r⁻¹ ^ n
z0s : Complex.abs (z0 - c0) = r
w0m : Complex.abs w0 < r
zcw : Complex.abs (z0 - (c0 + w0)) ≥ r - Complex.abs w0
zcw' : (Complex.abs (z0 - (c0 + w0)))⁻¹ ≤ (r - Complex.abs w0)⁻¹
a : (Complex.abs (2 * ↑π * I))⁻¹ = (2 * π)⁻¹
⊢ 2 * π * (2 * π)⁻¹ * (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 ^ n * r⁻¹ ^ n) =
    (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 / r) ^ n
Tactic:
rw [mul_inv_cancel Real.two_pi_pos.ne', ← mul_pow, ← div_eq_mul_inv _ r, one_mul]
State after:
no goals