internlm/Lean-Github huggingface dataset:
Theorem: cauchy1_bound
Proof 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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
isb : ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ 2 * π * r * (r⁻¹ ^ n * r⁻¹ * b)
⊢ 2 * π * b * r⁻¹ ^ n * 1 = 2 * π * b * r⁻¹ ^ n
Tactic:
simp
Proof state after:
no goals
Theorem: cauchy1_bound
Proof state before:
case refine_1
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
⊢ ContinuousOn (fun z => (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) (sphere c r)
Tactic:
apply ContinuousOn.smul
Proof state after:
case refine_1.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
⊢ ContinuousOn (fun x => (x - c)⁻¹ ^ n) (sphere c r)

case refine_1.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
⊢ ContinuousOn (fun x => (x - c)⁻¹ • f x) (sphere c r)
Theorem: cauchy1_bound
Proof state before:
case refine_1.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
⊢ ContinuousOn (fun x => (x - c)⁻¹ ^ n) (sphere c r)

case refine_1.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
⊢ ContinuousOn (fun x => (x - c)⁻¹ • f x) (sphere c r)
Tactic:
apply ContinuousOn.pow
Proof state after:
case refine_1.hf.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
⊢ ContinuousOn (fun x => (x - c)⁻¹) (sphere c r)

case refine_1.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
⊢ ContinuousOn (fun x => (x - c)⁻¹ • f x) (sphere c r)
Theorem: cauchy1_bound
Proof state before:
case refine_1.hf.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
⊢ ContinuousOn (fun x => (x - c)⁻¹) (sphere c r)

case refine_1.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
⊢ ContinuousOn (fun x => (x - c)⁻¹ • f x) (sphere c r)
Tactic:
exact ContinuousOn.inv_sphere rp
Proof state after:
case refine_1.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
⊢ ContinuousOn (fun x => (x - c)⁻¹ • f x) (sphere c r)
Theorem: cauchy1_bound
Proof state before:
case refine_1.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
⊢ ContinuousOn (fun x => (x - c)⁻¹ • f x) (sphere c r)
Tactic:
apply ContinuousOn.smul
Proof state after:
case refine_1.hg.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
⊢ ContinuousOn (fun x => (x - c)⁻¹) (sphere c r)

case refine_1.hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
⊢ ContinuousOn (fun x => f x) (sphere c r)
Theorem: cauchy1_bound
Proof state before:
case refine_1.hg.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
⊢ ContinuousOn (fun x => (x - c)⁻¹) (sphere c r)

case refine_1.hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
⊢ ContinuousOn (fun x => f x) (sphere c r)
Tactic:
exact ContinuousOn.inv_sphere rp
Proof state after:
case refine_1.hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
⊢ ContinuousOn (fun x => f x) (sphere c r)
Theorem: cauchy1_bound
Proof state before:
case refine_1.hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
⊢ ContinuousOn (fun x => f x) (sphere c r)
Tactic:
assumption
Proof state after:
no goals
Theorem: cauchy1_bound'
Proof 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
Proof 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
Theorem: cauchy1_bound'
Proof 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]
Proof 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
Theorem: cauchy1_bound'
Proof 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']
Proof state after:
no goals
Theorem: cauchy1_bound'
Proof 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]
Proof 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 ≤ π
Theorem: cauchy1_bound'
Proof 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
Proof state after:
no goals
Theorem: cauchy1_bound'
Proof 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]
Proof state after:
no goals
Theorem: cauchy1_bound'
Proof 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
Proof state after:
no goals
Theorem: cauchy1_bound'
Proof 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']
Proof state after:
no goals
Theorem: cauchy2_hasSum_n1n0_bound
Proof 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
Proof 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
Theorem: cauchy2_hasSum_n1n0_bound
Proof 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
Proof 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
Theorem: cauchy2_hasSum_n1n0_bound
Proof 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]
Proof 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
Theorem: cauchy2_hasSum_n1n0_bound
Proof 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
Proof 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
Theorem: cauchy2_hasSum_n1n0_bound
Proof 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
Proof 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
Theorem: cauchy2_hasSum_n1n0_bound
Proof 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]
Proof 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
Theorem: cauchy2_hasSum_n1n0_bound
Proof 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]
Proof state after:
no goals
Theorem: cauchy2_hasSum_n1n0_bound
Proof 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]
Proof state after:
no goals
Theorem: cauchy2_hasSum_n1n0_bound
Proof 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
Proof state after:
no goals