internlm/Lean-Github huggingface dataset:
Theorem: cauchy2_hasSum_n1n0
Proof state before:
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)
Tactic:
exact ContinuousOn.inv_sphere_ball w0m
Proof state after:
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)
Theorem: cauchy2_hasSum_n1n0
Proof state before:
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)
Tactic:
apply ContinuousOn.cauchy1 h.rp
Proof state after:
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 f (sphere c0 r ×ˢ sphere c1 r)
Theorem: cauchy2_hasSum_n1n0
Proof state before:
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 f (sphere c0 r ×ˢ sphere c1 r)
Tactic:
apply ContinuousOn.mono h.fc h.rs'
Proof state after:
no goals
Theorem: cauchy2_hasSum_n1n0
Proof state before:
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
Tactic:
rw [← hs]
Proof state after:
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 •
            (2 * ↑π * I)⁻¹ • (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
Theorem: cauchy2_hasSum_n1n0
Proof state before:
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 •
            (2 * ↑π * I)⁻¹ • (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
Tactic:
exact fun n z0 z0s ↦ cauchy2_hasSum_n1n0_bound h w0m n z0s
Proof state after:
no goals
Theorem: cauchy2_hasSum_n1n0
Proof state before:
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
Tactic:
apply Summable.mul_left
Proof state after:
case hf.bs.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
⊢ Summable fun i => (Complex.abs w1 / r) ^ i
Theorem: cauchy2_hasSum_n1n0
Proof state before:
case hf.bs.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
⊢ Summable fun i => (Complex.abs w1 / r) ^ i
Tactic:
apply summable_geometric_of_abs_lt_one
Proof state after:
case hf.bs.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
⊢ |Complex.abs w1 / r| < 1
Theorem: cauchy2_hasSum_n1n0
Proof state before:
case hf.bs.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
⊢ |Complex.abs w1 / r| < 1
Tactic:
rw [abs_div, abs_of_pos h.rp]
Proof state after:
case hf.bs.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
⊢ |Complex.abs w1| / r < 1
Theorem: cauchy2_hasSum_n1n0
Proof state before:
case hf.bs.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
⊢ |Complex.abs w1| / r < 1
Tactic:
simp at w1m ⊢
Proof state after:
case hf.bs.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
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
w1m : Complex.abs w1 < r
⊢ Complex.abs w1 / r < 1
Theorem: cauchy2_hasSum_n1n0
Proof state before:
case hf.bs.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
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
w1m : Complex.abs w1 < r
⊢ Complex.abs w1 / r < 1
Tactic:
exact (div_lt_one h.rp).mpr w1m
Proof state after:
no goals
Theorem: cauchy2_hasSum_n1n0
Proof state before:
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))
Tactic:
intro z0 z0s
Proof state after:
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
z0 : ℂ
z0s : z0 ∈ sphere c0 r
⊢ HasSum (fun n => w1 ^ n • s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1))
    (s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Theorem: cauchy2_hasSum_n1n0
Proof state before:
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
z0 : ℂ
z0s : z0 ∈ sphere c0 r
⊢ HasSum (fun n => w1 ^ n • s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1))
    (s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
simp_rw [smul_comm s _]
Proof state after:
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
z0 : ℂ
z0s : z0 ∈ sphere c0 r
⊢ HasSum (fun n => w1 ^ n • (z0 - (c0 + w0))⁻¹ • s • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1))
    ((z0 - (c0 + w0))⁻¹ • s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Theorem: cauchy2_hasSum_n1n0
Proof state before:
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
z0 : ℂ
z0s : z0 ∈ sphere c0 r
⊢ HasSum (fun n => w1 ^ n • (z0 - (c0 + w0))⁻¹ • s • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1))
    ((z0 - (c0 + w0))⁻¹ • s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
simp_rw [smul_comm (w1 ^ _) _]
Proof state after:
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
z0 : ℂ
z0s : z0 ∈ sphere c0 r
⊢ HasSum (fun n => (z0 - (c0 + w0))⁻¹ • s • w1 ^ n • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1))
    ((z0 - (c0 + w0))⁻¹ • s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Theorem: cauchy2_hasSum_n1n0
Proof state before:
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
z0 : ℂ
z0s : z0 ∈ sphere c0 r
⊢ HasSum (fun n => (z0 - (c0 + w0))⁻¹ • s • w1 ^ n • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1))
    ((z0 - (c0 + w0))⁻¹ • s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
apply HasSum.const_smul
Proof state after:
case hf.h.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
z0 : ℂ
z0s : z0 ∈ sphere c0 r
⊢ HasSum (fun i => s • w1 ^ i • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Theorem: cauchy2_hasSum_n1n0
Proof state before:
case hf.h.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
z0 : ℂ
z0s : z0 ∈ sphere c0 r
⊢ HasSum (fun i => s • w1 ^ i • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
have fcs : ContinuousOn (fun z1 ↦ f (z0, z1)) (sphere c1 r) :=
  ContinuousOn.mono (h.fc1 (Metric.sphere_subset_closedBall z0s))
    Metric.sphere_subset_closedBall
Proof state after:
case hf.h.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
z0 : ℂ
z0s : z0 ∈ sphere c0 r
fcs : ContinuousOn (fun z1 => f (z0, z1)) (sphere c1 r)
⊢ HasSum (fun i => s • w1 ^ i • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Theorem: cauchy2_hasSum_n1n0
Proof state before:
case hf.h.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
z0 : ℂ
z0s : z0 ∈ sphere c0 r
fcs : ContinuousOn (fun z1 => f (z0, z1)) (sphere c1 r)
⊢ HasSum (fun i => s • w1 ^ i • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
have hs1 := cauchy1_hasSum h.rp fcs w1m
Proof state after:
case hf.h.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
z0 : ℂ
z0s : z0 ∈ sphere c0 r
fcs : ContinuousOn (fun z1 => f (z0, z1)) (sphere c1 r)
hs1 :
  HasSum (fun n => w1 ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z))
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - (c1 + w1))⁻¹ • f (z0, z))
⊢ HasSum (fun i => s • w1 ^ i • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Theorem: cauchy2_hasSum_n1n0
Proof state before:
case hf.h.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
z0 : ℂ
z0s : z0 ∈ sphere c0 r
fcs : ContinuousOn (fun z1 => f (z0, z1)) (sphere c1 r)
hs1 :
  HasSum (fun n => w1 ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z))
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - (c1 + w1))⁻¹ • f (z0, z))
⊢ HasSum (fun i => s • w1 ^ i • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
simp_rw [hs, smul_comm _ s] at hs1
Proof state after:
case hf.h.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
z0 : ℂ
z0s : z0 ∈ sphere c0 r
fcs : ContinuousOn (fun z1 => f (z0, z1)) (sphere c1 r)
hs1 :
  HasSum (fun n => s • w1 ^ n • ∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z))
    (s • ∮ (z : ℂ) in C(c1, r), (z - (c1 + w1))⁻¹ • f (z0, z))
⊢ HasSum (fun i => s • w1 ^ i • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Theorem: cauchy2_hasSum_n1n0
Proof state before:
case hf.h.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
z0 : ℂ
z0s : z0 ∈ sphere c0 r
fcs : ContinuousOn (fun z1 => f (z0, z1)) (sphere c1 r)
hs1 :
  HasSum (fun n => s • w1 ^ n • ∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z))
    (s • ∮ (z : ℂ) in C(c1, r), (z - (c1 + w1))⁻¹ • f (z0, z))
⊢ HasSum (fun i => s • w1 ^ i • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
assumption
Proof state after:
no goals
Theorem: series2Coeff_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
n0 n1 : ℕ
⊢ ‖h.series2Coeff n0 n1‖ ≤ b * r⁻¹ ^ (n0 + n1)
Tactic:
have inner_c :
  ContinuousOn
    (fun z0 ↦ (2 * π * I : ℂ)⁻¹ • ∮ z1 in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r) :=
  ContinuousOn.smul continuousOn_const (ContinuousOn.cauchy1 h.rp (ContinuousOn.mono h.fc h.rs'))
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
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
⊢ ‖h.series2Coeff n0 n1‖ ≤ b * r⁻¹ ^ (n0 + n1)
Theorem: series2Coeff_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
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
⊢ ‖h.series2Coeff n0 n1‖ ≤ b * r⁻¹ ^ (n0 + n1)
Tactic:
have inner_b : ∀ z0 _, ‖(2*π*I : ℂ)⁻¹ • ∮ z1 in C(c1, r),
    (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0,z1)‖ ≤ b * r⁻¹ ^ n1 :=
  fun z0 z0s ↦ cauchy1_bound' h.rp b
    (ContinuousOn.mono (h.fc1 (mem_sphere_closed z0s)) Metric.sphere_subset_closedBall)
    (fun z1 ↦ h.fb z0s) n1
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
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
inner_b :
  ∀ z0 ∈ sphere c0 r,
    ‖(2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤ b * r⁻¹ ^ n1
⊢ ‖h.series2Coeff n0 n1‖ ≤ b * r⁻¹ ^ (n0 + n1)
Theorem: series2Coeff_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
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
inner_b :
  ∀ z0 ∈ sphere c0 r,
    ‖(2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤ b * r⁻¹ ^ n1
⊢ ‖h.series2Coeff n0 n1‖ ≤ b * r⁻¹ ^ (n0 + n1)
Tactic:
have outer := cauchy1_bound' h.rp _ inner_c inner_b n0
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
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
inner_b :
  ∀ z0 ∈ sphere c0 r,
    ‖(2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤ b * r⁻¹ ^ n1
outer :
  ‖(2 * ↑π * I)⁻¹ •
        ∮ (z : ℂ) in C(c0, r),
          (z - c0)⁻¹ ^ n0 •
            (z - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
    b * r⁻¹ ^ n1 * r⁻¹ ^ n0
⊢ ‖h.series2Coeff n0 n1‖ ≤ b * r⁻¹ ^ (n0 + n1)
Theorem: series2Coeff_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
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
inner_b :
  ∀ z0 ∈ sphere c0 r,
    ‖(2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤ b * r⁻¹ ^ n1
outer :
  ‖(2 * ↑π * I)⁻¹ •
        ∮ (z : ℂ) in C(c0, r),
          (z - c0)⁻¹ ^ n0 •
            (z - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
    b * r⁻¹ ^ n1 * r⁻¹ ^ n0
⊢ ‖h.series2Coeff n0 n1‖ ≤ b * r⁻¹ ^ (n0 + n1)
Tactic:
have e : b * r⁻¹ ^ n1 * r⁻¹ ^ n0 = b * r⁻¹ ^ (n0 + n1) := by
  rw [mul_assoc, ← pow_add, add_comm n0 _]
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
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
inner_b :
  ∀ z0 ∈ sphere c0 r,
    ‖(2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤ b * r⁻¹ ^ n1
outer :
  ‖(2 * ↑π * I)⁻¹ •
        ∮ (z : ℂ) in C(c0, r),
          (z - c0)⁻¹ ^ n0 •
            (z - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
    b * r⁻¹ ^ n1 * r⁻¹ ^ n0
e : b * r⁻¹ ^ n1 * r⁻¹ ^ n0 = b * r⁻¹ ^ (n0 + n1)
⊢ ‖h.series2Coeff n0 n1‖ ≤ b * r⁻¹ ^ (n0 + n1)