internlm/Lean-Github huggingface dataset:
Theorem: Separate.fd1
Proof state before:
case a
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 ∈ closedBall c0 r
w1m : w1 ∈ closedBall c1 r
⊢ (w0, w1) ∈ closedBall c0 r ×ˢ closedBall c1 r
Tactic:
exact Set.mem_prod.mpr ⟨w0m, w1m⟩
Proof state after:
no goals
Theorem: cauchy1
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b r : ℝ
c w : ℂ
f : ℂ → E
wm : w ∈ ball c r
fc : ContinuousOn f (closedBall c r)
fd : ∀ z ∈ ball c r, DifferentiableAt ℂ f z
⊢ ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - w)⁻¹ • f z) = f w
Tactic:
refine Complex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
  Set.countable_empty wm fc ?_
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b r : ℝ
c w : ℂ
f : ℂ → E
wm : w ∈ ball c r
fc : ContinuousOn f (closedBall c r)
fd : ∀ z ∈ ball c r, DifferentiableAt ℂ f z
⊢ ∀ x ∈ ball c r \ ∅, DifferentiableAt ℂ (fun z => f z) x
Theorem: cauchy1
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b r : ℝ
c w : ℂ
f : ℂ → E
wm : w ∈ ball c r
fc : ContinuousOn f (closedBall c r)
fd : ∀ z ∈ ball c r, DifferentiableAt ℂ f z
⊢ ∀ x ∈ ball c r \ ∅, DifferentiableAt ℂ (fun z => f z) x
Tactic:
intro z zm
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b r : ℝ
c w : ℂ
f : ℂ → E
wm : w ∈ ball c r
fc : ContinuousOn f (closedBall c r)
fd : ∀ z ∈ ball c r, DifferentiableAt ℂ f z
z : ℂ
zm : z ∈ ball c r \ ∅
⊢ DifferentiableAt ℂ (fun z => f z) z
Theorem: cauchy1
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b r : ℝ
c w : ℂ
f : ℂ → E
wm : w ∈ ball c r
fc : ContinuousOn f (closedBall c r)
fd : ∀ z ∈ ball c r, DifferentiableAt ℂ f z
z : ℂ
zm : z ∈ ball c r \ ∅
⊢ DifferentiableAt ℂ (fun z => f z) z
Tactic:
apply fd z _
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b r : ℝ
c w : ℂ
f : ℂ → E
wm : w ∈ ball c r
fc : ContinuousOn f (closedBall c r)
fd : ∀ z ∈ ball c r, DifferentiableAt ℂ f z
z : ℂ
zm : z ∈ ball c r \ ∅
⊢ z ∈ ball c r
Theorem: cauchy1
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b r : ℝ
c w : ℂ
f : ℂ → E
wm : w ∈ ball c r
fc : ContinuousOn f (closedBall c r)
fd : ∀ z ∈ ball c r, DifferentiableAt ℂ f z
z : ℂ
zm : z ∈ ball c r \ ∅
⊢ z ∈ ball c r
Tactic:
simp only [Metric.mem_ball, Set.diff_empty] at zm ⊢
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b r : ℝ
c w : ℂ
f : ℂ → E
wm : w ∈ ball c r
fc : ContinuousOn f (closedBall c r)
fd : ∀ z ∈ ball c r, DifferentiableAt ℂ f z
z : ℂ
zm : dist z c < r
⊢ dist z c < r
Theorem: cauchy1
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b r : ℝ
c w : ℂ
f : ℂ → E
wm : w ∈ ball c r
fc : ContinuousOn f (closedBall c r)
fd : ∀ z ∈ ball c r, DifferentiableAt ℂ f z
z : ℂ
zm : dist z c < r
⊢ dist z c < r
Tactic:
assumption
Proof state after:
no goals
Theorem: cauchy2
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 c0 r
w1m : w1 ∈ ball c1 r
⊢ ((2 * ↑π * I)⁻¹ •
      ∮ (z0 : ℂ) in C(c0, r), (z0 - w0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) =
    f (w0, w1)
Tactic:
have h1 := fun z0 (z0m : z0 ∈ closedBall c0 r) ↦
  cauchy1 w1m (h.fc1 z0m) fun z1 z1m ↦ h.fd1 z0m (mem_open_closed z1m)
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 c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
⊢ ((2 * ↑π * I)⁻¹ •
      ∮ (z0 : ℂ) in C(c0, r), (z0 - w0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) =
    f (w0, w1)
Theorem: cauchy2
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 c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
⊢ ((2 * ↑π * I)⁻¹ •
      ∮ (z0 : ℂ) in C(c0, r), (z0 - w0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) =
    f (w0, w1)
Tactic:
have ic1 : ContinuousOn (fun z0 ↦ (2 * π * I : ℂ)⁻¹ • ∮ z1 in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1))
    (closedBall c0 r) :=
  (h.fc0 w1m).congr h1
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 c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
⊢ ((2 * ↑π * I)⁻¹ •
      ∮ (z0 : ℂ) in C(c0, r), (z0 - w0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) =
    f (w0, w1)
Theorem: cauchy2
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 c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
⊢ ((2 * ↑π * I)⁻¹ •
      ∮ (z0 : ℂ) in C(c0, r), (z0 - w0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) =
    f (w0, w1)
Tactic:
have id1 : DifferentiableOn ℂ (fun z0 ↦ (2 * π * I : ℂ)⁻¹ • ∮ z1 in C(c1, r), (z1 - w1)⁻¹
    • f (z0, z1)) (ball c0 r) := by
  rw [differentiableOn_congr fun z zs ↦ h1 z (mem_open_closed zs)]
  intro z0 z0m; apply DifferentiableAt.differentiableWithinAt
  exact h.fd0 (mem_open_closed z0m) (mem_open_closed 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 c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
id1 : DifferentiableOn ℂ (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (ball c0 r)
⊢ ((2 * ↑π * I)⁻¹ •
      ∮ (z0 : ℂ) in C(c0, r), (z0 - w0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) =
    f (w0, w1)
Theorem: cauchy2
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 c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
id1 : DifferentiableOn ℂ (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (ball c0 r)
⊢ ((2 * ↑π * I)⁻¹ •
      ∮ (z0 : ℂ) in C(c0, r), (z0 - w0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) =
    f (w0, w1)
Tactic:
have h01 :=
  cauchy1 w0m ic1 fun z0 z0m ↦
    DifferentiableOn.differentiableAt id1 (IsOpen.mem_nhds isOpen_ball z0m)
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 c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
id1 : DifferentiableOn ℂ (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (ball c0 r)
h01 :
  ((2 * ↑π * I)⁻¹ •
      ∮ (z : ℂ) in C(c0, r), (z - w0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z, z1)) =
    (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (w0, z1)
⊢ ((2 * ↑π * I)⁻¹ •
      ∮ (z0 : ℂ) in C(c0, r), (z0 - w0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) =
    f (w0, w1)
Theorem: cauchy2
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 c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
id1 : DifferentiableOn ℂ (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (ball c0 r)
h01 :
  ((2 * ↑π * I)⁻¹ •
      ∮ (z : ℂ) in C(c0, r), (z - w0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z, z1)) =
    (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (w0, z1)
⊢ ((2 * ↑π * I)⁻¹ •
      ∮ (z0 : ℂ) in C(c0, r), (z0 - w0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) =
    f (w0, w1)
Tactic:
exact _root_.trans h01 (h1 w0 (mem_open_closed w0m))
Proof state after:
no goals
Theorem: cauchy2
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 c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
⊢ DifferentiableOn ℂ (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (ball c0 r)
Tactic:
rw [differentiableOn_congr fun z zs ↦ h1 z (mem_open_closed zs)]
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 c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
⊢ DifferentiableOn ℂ (fun z => f (z, w1)) (ball c0 r)
Theorem: cauchy2
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 c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
⊢ DifferentiableOn ℂ (fun z => f (z, w1)) (ball c0 r)
Tactic:
intro z0 z0m
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 c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
z0 : ℂ
z0m : z0 ∈ ball c0 r
⊢ DifferentiableWithinAt ℂ (fun z => f (z, w1)) (ball c0 r) z0
Theorem: cauchy2
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 c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
z0 : ℂ
z0m : z0 ∈ ball c0 r
⊢ DifferentiableWithinAt ℂ (fun z => f (z, w1)) (ball c0 r) z0
Tactic:
apply DifferentiableAt.differentiableWithinAt
Proof state after:
case 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 c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
z0 : ℂ
z0m : z0 ∈ ball c0 r
⊢ DifferentiableAt ℂ (fun z => f (z, w1)) z0
Theorem: cauchy2
Proof state before:
case 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 c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
z0 : ℂ
z0m : z0 ∈ ball c0 r
⊢ DifferentiableAt ℂ (fun z => f (z, w1)) z0
Tactic:
exact h.fd0 (mem_open_closed z0m) (mem_open_closed w1m)
Proof state after:
no goals
Theorem: cauchy1_hasSum
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
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : w ∈ ball 0 r
⊢ HasSum (fun n => w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
Tactic:
simp at wm
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
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
⊢ HasSum (fun n => w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
Theorem: cauchy1_hasSum
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
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
⊢ HasSum (fun n => w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
Tactic:
have ci : CircleIntegrable f c r := ContinuousOn.circleIntegrable (by linarith) fc
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
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
⊢ HasSum (fun n => w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
Theorem: cauchy1_hasSum
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
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
⊢ HasSum (fun n => w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
Tactic:
have h := hasSum_cauchyPowerSeries_integral ci wm
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
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
h :
  HasSum (fun n => (cauchyPowerSeries f c r n) fun x => w)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
⊢ HasSum (fun n => w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
Theorem: cauchy1_hasSum
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
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
h :
  HasSum (fun n => (cauchyPowerSeries f c r n) fun x => w)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
⊢ HasSum (fun n => w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
Tactic:
simp_rw [cauchyPowerSeries_apply] at h
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
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
h :
  HasSum (fun n => (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
⊢ HasSum (fun n => w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
Theorem: cauchy1_hasSum
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
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
h :
  HasSum (fun n => (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
⊢ HasSum (fun n => w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
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 : ℝ
f : ℂ → E
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
h :
  HasSum (fun n => (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
Theorem: cauchy1_hasSum
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
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
h :
  HasSum (fun n => (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
Tactic:
simp_rw [hs] at h
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
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
h :
  HasSum (fun n => s • ∮ (z : ℂ) in C(c, r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
⊢ HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
Theorem: cauchy1_hasSum
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
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
h :
  HasSum (fun n => s • ∮ (z : ℂ) in C(c, r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
⊢ HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
Tactic:
generalize hg : (s • ∮ z : ℂ in C(c, r), (z - (c + w))⁻¹ • f z) = g
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
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
h :
  HasSum (fun n => s • ∮ (z : ℂ) in C(c, r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
g : E
hg : (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z) = g
⊢ HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) g
Theorem: cauchy1_hasSum
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
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
h :
  HasSum (fun n => s • ∮ (z : ℂ) in C(c, r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
g : E
hg : (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z) = g
⊢ HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) g
Tactic:
rw [hg] at h
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
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
g : E
h : HasSum (fun n => s • ∮ (z : ℂ) in C(c, r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) g
hg : (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z) = g
⊢ HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) g