Theorem: cauchy1_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✝ : ℝ
f : ℂ → E
r : ℝ
c : ℂ
rp : r > 0
b : ℝ
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
⊢ ‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ b * r⁻¹ ^ n
Tactic:
have a : abs (2*π*I : ℂ)⁻¹ = (2*π)⁻¹ := by
  simp only [mul_inv_rev, Complex.inv_I, neg_mul, map_neg_eq_map, map_mul, Complex.abs_I,
    map_inv₀, Complex.abs_ofReal, Complex.abs_two, one_mul, mul_eq_mul_right_iff, inv_inj,
    abs_eq_self, inv_eq_zero, OfNat.ofNat_ne_zero, or_false]
  exact Real.pi_pos.le
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
r : ℝ
c : ℂ
rp : r > 0
b : ℝ
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
a : Complex.abs (2 * ↑π * I)⁻¹ = (2 * π)⁻¹
⊢ ‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ b * 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✝ : ℝ
f : ℂ → E
r : ℝ
c : ℂ
rp : r > 0
b : ℝ
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
a : Complex.abs (2 * ↑π * I)⁻¹ = (2 * π)⁻¹
⊢ ‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ b * r⁻¹ ^ n
Tactic:
rw [norm_smul, Complex.norm_eq_abs, a]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
r : ℝ
c : ℂ
rp : r > 0
b : ℝ
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
a : Complex.abs (2 * ↑π * I)⁻¹ = (2 * π)⁻¹
⊢ (2 * π)⁻¹ * ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ b * 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✝ : ℝ
f : ℂ → E
r : ℝ
c : ℂ
rp : r > 0
b : ℝ
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
a : Complex.abs (2 * ↑π * I)⁻¹ = (2 * π)⁻¹
⊢ (2 * π)⁻¹ * ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ b * r⁻¹ ^ n
Tactic:
calc (2*π)⁻¹ * ‖∮ z in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖
  _ ≤ (2*π)⁻¹ * (2*π * b * r⁻¹ ^ n) := by bound [cauchy1_bound rp fc bh n]
  _ = (2*π)⁻¹ * (2*π) * b * r⁻¹ ^ n := by ring
  _ = b * r⁻¹ ^ n := by field_simp [Real.pi_pos.ne']
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✝ : ℝ
f : ℂ → E
r : ℝ
c : ℂ
rp : r > 0
b : ℝ
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
⊢ Complex.abs (2 * ↑π * I)⁻¹ = (2 * π)⁻¹
Tactic:
simp only [mul_inv_rev, Complex.inv_I, neg_mul, map_neg_eq_map, map_mul, Complex.abs_I,
  map_inv₀, Complex.abs_ofReal, Complex.abs_two, one_mul, 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✝ : ℝ
f : ℂ → E
r : ℝ
c : ℂ
rp : r > 0
b : ℝ
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
⊢ 0 ≤ π

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
r : ℝ
c : ℂ
rp : r > 0
b : ℝ
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
⊢ 0 ≤ π
Tactic:
exact Real.pi_pos.le
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✝ : ℝ
f : ℂ → E
r : ℝ
c : ℂ
rp : r > 0
b : ℝ
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
a : Complex.abs (2 * ↑π * I)⁻¹ = (2 * π)⁻¹
⊢ (2 * π)⁻¹ * ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ (2 * π)⁻¹ * (2 * π * b * r⁻¹ ^ n)
Tactic:
bound [cauchy1_bound rp fc bh n]
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✝ : ℝ
f : ℂ → E
r : ℝ
c : ℂ
rp : r > 0
b : ℝ
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
a : Complex.abs (2 * ↑π * I)⁻¹ = (2 * π)⁻¹
⊢ (2 * π)⁻¹ * (2 * π * b * r⁻¹ ^ n) = (2 * π)⁻¹ * (2 * π) * b * 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✝ : ℝ
f : ℂ → E
r : ℝ
c : ℂ
rp : r > 0
b : ℝ
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
a : Complex.abs (2 * ↑π * I)⁻¹ = (2 * π)⁻¹
⊢ (2 * π)⁻¹ * (2 * π) * b * r⁻¹ ^ n = b * r⁻¹ ^ n
Tactic:
field_simp [Real.pi_pos.ne']
State after:
no goals