internlm/Lean-Github huggingface dataset:
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) - Complex.abs (-w0)
Tactic:
bound
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) - Complex.abs (-w0) = r - Complex.abs w0
Tactic:
rw [z0s]
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
⊢ r - Complex.abs (-w0) = r - Complex.abs w0
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
⊢ r - Complex.abs (-w0) = r - Complex.abs w0
Tactic:
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
zcw : Complex.abs (z0 - (c0 + w0)) ≥ r - Complex.abs w0
⊢ (Complex.abs (z0 - (c0 + w0)))⁻¹ ≤ (r - Complex.abs w0)⁻¹
Tactic:
bound
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
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]
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)⁻¹
⊢ 0 ≤ π
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)⁻¹
⊢ 0 ≤ π
Tactic:
bound
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
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
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
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
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
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
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
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]
Proof state after:
no goals
Theorem: cauchy2_hasSum_n1n0
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
w1m : w1 ∈ ball 0 r
⊢ HasSum (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) (f (c0 + w0, c1 + w1))
Tactic:
have cw0m : c0 + w0 ∈ ball c0 r := by
  simpa only [Metric.mem_ball, dist_self_add_left, Complex.norm_eq_abs, Complex.dist_eq,
    sub_zero] using 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
⊢ HasSum (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) (f (c0 + w0, c1 + w1))
Theorem: cauchy2_hasSum_n1n0
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
⊢ HasSum (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) (f (c0 + w0, c1 + w1))
Tactic:
have cw1m : c1 + w1 ∈ ball c1 r := by
  simpa only [Metric.mem_ball, dist_self_add_left, Complex.norm_eq_abs, dist_zero_right] using w1m
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
⊢ HasSum (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) (f (c0 + w0, c1 + w1))
Theorem: cauchy2_hasSum_n1n0
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
⊢ HasSum (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) (f (c0 + w0, c1 + w1))
Tactic:
simp_rw [Separate.series2CoeffN0Sum]
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
⊢ HasSum
    (fun n1 =>
      w1 ^ n1 •
        (2 * ↑π * I)⁻¹ •
          ∮ (z0 : ℂ) in C(c0, r),
            (z0 - (c0 + w0))⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (f (c0 + w0, c1 + w1))
Theorem: cauchy2_hasSum_n1n0
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
⊢ HasSum
    (fun n1 =>
      w1 ^ n1 •
        (2 * ↑π * I)⁻¹ •
          ∮ (z0 : ℂ) in C(c0, r),
            (z0 - (c0 + w0))⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (f (c0 + w0, c1 + w1))
Tactic:
rw [← cauchy2 h cw0m cw1m]
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
⊢ HasSum
    (fun n1 =>
      w1 ^ n1 •
        (2 * ↑π * I)⁻¹ •
          ∮ (z0 : ℂ) in C(c0, r),
            (z0 - (c0 + w0))⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    ((2 * ↑π * I)⁻¹ •
      ∮ (z0 : ℂ) in C(c0, r),
        (z0 - (c0 + w0))⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Theorem: cauchy2_hasSum_n1n0
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
⊢ HasSum
    (fun n1 =>
      w1 ^ n1 •
        (2 * ↑π * I)⁻¹ •
          ∮ (z0 : ℂ) in C(c0, r),
            (z0 - (c0 + w0))⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    ((2 * ↑π * I)⁻¹ •
      ∮ (z0 : ℂ) in C(c0, r),
        (z0 - (c0 + w0))⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
generalize hs : (2 * ↑π * I)⁻¹ = s
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ HasSum
    (fun n1 =>
      w1 ^ n1 •
        s •
          ∮ (z0 : ℂ) in C(c0, r),
            (z0 - (c0 + w0))⁻¹ • s • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z0 : ℂ) in C(c0, r), (z0 - (c0 + w0))⁻¹ • s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Theorem: cauchy2_hasSum_n1n0
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ HasSum
    (fun n1 =>
      w1 ^ n1 •
        s •
          ∮ (z0 : ℂ) in C(c0, r),
            (z0 - (c0 + w0))⁻¹ • s • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z0 : ℂ) in C(c0, r), (z0 - (c0 + w0))⁻¹ • s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
simp_rw [smul_comm _ s _]
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ HasSum
    (fun n1 =>
      s •
        w1 ^ n1 •
          ∮ (z0 : ℂ) in C(c0, r),
            s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z0 : ℂ) in C(c0, r), s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Theorem: cauchy2_hasSum_n1n0
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ HasSum
    (fun n1 =>
      s •
        w1 ^ n1 •
          ∮ (z0 : ℂ) in C(c0, r),
            s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z0 : ℂ) in C(c0, r), s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
apply HasSum.const_smul
Proof state after:
case hf
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ HasSum
    (fun i =>
      w1 ^ i •
        ∮ (z0 : ℂ) in C(c0, r),
          s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z0, z1))
    (∮ (z0 : ℂ) in C(c0, r), s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Theorem: cauchy2_hasSum_n1n0
Proof state before:
case hf
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ HasSum
    (fun i =>
      w1 ^ i •
        ∮ (z0 : ℂ) in C(c0, r),
          s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z0, z1))
    (∮ (z0 : ℂ) in C(c0, r), s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
simp_rw [← circleIntegral.integral_smul (w1 ^ _) _ _ _]
Proof state after:
case hf
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ HasSum
    (fun i =>
      ∮ (z : ℂ) in C(c0, r),
        w1 ^ i • s • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z, z1))
    (∮ (z0 : ℂ) in C(c0, r), s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Theorem: cauchy2_hasSum_n1n0
Proof state before:
case hf
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ HasSum
    (fun i =>
      ∮ (z : ℂ) in C(c0, r),
        w1 ^ i • s • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z, z1))
    (∮ (z0 : ℂ) in C(c0, r), s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
apply sum_integral_commute (fun n ↦ (r - abs w0)⁻¹ * b * (abs w1 / r) ^ n) h.rp
Proof state after:
case hf.fc
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ ∀ (n : ℕ),
    ContinuousOn
      (fun z => w1 ^ n • s • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z, z1))
      (sphere c0 r)

case hf.fb
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ ∀ (n : ℕ),
    ∀ z ∈ sphere c0 r,
      ‖w1 ^ n • s • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
        (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 / r) ^ n

case hf.bs
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ Summable fun n => (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 / r) ^ n

case hf.h
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ ∀ z ∈ sphere c0 r,
    HasSum (fun n => w1 ^ n • s • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z, z1))
      (s • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z, z1))
Theorem: cauchy2_hasSum_n1n0
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
w1m : w1 ∈ ball 0 r
⊢ c0 + w0 ∈ ball c0 r
Tactic:
simpa only [Metric.mem_ball, dist_self_add_left, Complex.norm_eq_abs, Complex.dist_eq,
  sub_zero] using w0m
Proof state after:
no goals
Theorem: cauchy2_hasSum_n1n0
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
⊢ c1 + w1 ∈ ball c1 r
Tactic:
simpa only [Metric.mem_ball, dist_self_add_left, Complex.norm_eq_abs, dist_zero_right] using w1m
Proof state after:
no goals
Theorem: cauchy2_hasSum_n1n0
Proof state before:
case hf.fc
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ ∀ (n : ℕ),
    ContinuousOn
      (fun z => w1 ^ n • s • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z, z1))
      (sphere c0 r)
Tactic:
intro n
Proof state after:
case hf.fc
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
n : ℕ
⊢ ContinuousOn
    (fun z => w1 ^ n • s • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z, z1))
    (sphere c0 r)
Theorem: cauchy2_hasSum_n1n0
Proof state before:
case hf.fc
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
n : ℕ
⊢ ContinuousOn
    (fun z => w1 ^ n • s • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z, z1))
    (sphere c0 r)
Tactic:
apply ContinuousOn.smul continuousOn_const
Proof state after:
case hf.fc
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
n : ℕ
⊢ ContinuousOn (fun x => s • (x - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (x, z1))
    (sphere c0 r)
Theorem: cauchy2_hasSum_n1n0
Proof state before:
case hf.fc
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
n : ℕ
⊢ ContinuousOn (fun x => s • (x - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (x, z1))
    (sphere c0 r)
Tactic:
apply ContinuousOn.smul continuousOn_const
Proof state after:
case hf.fc
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
n : ℕ
⊢ ContinuousOn (fun x => (x - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (x, z1))
    (sphere c0 r)
Theorem: cauchy2_hasSum_n1n0
Proof state before:
case hf.fc
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
n : ℕ
⊢ ContinuousOn (fun x => (x - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (x, z1))
    (sphere c0 r)
Tactic:
apply ContinuousOn.smul
Proof state after:
case hf.fc.hf
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
n : ℕ
⊢ ContinuousOn (fun x => (x - (c0 + w0))⁻¹) (sphere c0 r)

case hf.fc.hg
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
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
n : ℕ
⊢ ContinuousOn (fun x => ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (x, z1)) (sphere c0 r)