internlm/Lean-Github huggingface dataset:
Theorem: Cauchy_formula
Proof state before:
case intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Tactic:
have hδ := fun z hz => hα z ((@closedBall_subset_ball ℂ _ c (α/2) α (by linarith)) hz)
Proof state after:
case intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Theorem: Cauchy_formula
Proof state before:
case intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Tactic:
obtain ⟨r, hr0, hrδ, hrR⟩ : ∃ r, 0 < r ∧ r ≤ δ ∧ r ≤ R :=
  ⟨min δ R, lt_min δ0 h0, min_le_left _ _, min_le_right _ _⟩
Proof state after:
case intro.intro.intro.intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Theorem: Cauchy_formula
Proof state before:
case intro.intro.intro.intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Tactic:
have hsub : closedBall c R \ ball c r ⊆ closedBall c R :=  diff_subset (closedBall c R) (ball c r)
Proof state after:
case intro.intro.intro.intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Theorem: Cauchy_formula
Proof state before:
case intro.intro.intro.intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Tactic:
have hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c} :=
  diff_subset_diff_right (singleton_subset_iff.2 <| mem_closedBall_self hr0.le)
Proof state after:
case intro.intro.intro.intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Theorem: Cauchy_formula
Proof state before:
case intro.intro.intro.intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Tactic:
have hzne : ∀ z ∈ sphere c r, z ≠ c := fun z hz =>
  ne_of_mem_of_not_mem hz fun h => hr0.ne' <| dist_self c ▸ Eq.symm h
Proof state after:
case intro.intro.intro.intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Theorem: Cauchy_formula
Proof state before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
⊢ Tendsto f (𝓝 c) (𝓝 y)
Tactic:
rw [← (@nhdsWithin_eq_nhds _ _ c (closedBall c R)).mpr (closedBall_mem_nhds _ h0)]
Proof state after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
⊢ Tendsto f (𝓝[closedBall c R] c) (𝓝 y)
Theorem: Cauchy_formula
Proof state before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
⊢ Tendsto f (𝓝[closedBall c R] c) (𝓝 y)
Tactic:
exact ContinuousOn.continuousWithinAt hf <| mem_closedBall_self (le_of_lt h0)
Proof state after:
no goals
Theorem: Cauchy_formula
Proof state before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
z : ℂ
hz : z ∈ closedBall c (α / 2)
⊢ α / 2 < α
Tactic:
linarith
Proof state after:
no goals
Theorem: Cauchy_formula
Proof state before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ =
    ‖(∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z) - ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • y‖
Tactic:
congr 2
Proof state after:
case e_a.e_a
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z

case e_a.e_a
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ (2 * ↑π * I) • y = ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • y
Theorem: Cauchy_formula
Proof state before:
case e_a.e_a
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z
Tactic:
refine circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable hr0
  hrR countable_empty  (hf.mono hsub) fun z hz => hdiff z ?_
Proof state after:
case e_a.e_a
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
z : ℂ
hz : z ∈ (ball c R \ closedBall c r) \ ∅
⊢ z ∈ ball c R
Theorem: Cauchy_formula
Proof state before:
case e_a.e_a
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
z : ℂ
hz : z ∈ (ball c R \ closedBall c r) \ ∅
⊢ z ∈ ball c R
Tactic:
apply mem_of_subset_of_mem _ hz
Proof state after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
z : ℂ
hz : z ∈ (ball c R \ closedBall c r) \ ∅
⊢ (ball c R \ closedBall c r) \ ∅ ⊆ ball c R
Theorem: Cauchy_formula
Proof state before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
z : ℂ
hz : z ∈ (ball c R \ closedBall c r) \ ∅
⊢ (ball c R \ closedBall c r) \ ∅ ⊆ ball c R
Tactic:
rw [diff_empty]
Proof state after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
z : ℂ
hz : z ∈ (ball c R \ closedBall c r) \ ∅
⊢ ball c R \ closedBall c r ⊆ ball c R
Theorem: Cauchy_formula
Proof state before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
z : ℂ
hz : z ∈ (ball c R \ closedBall c r) \ ∅
⊢ ball c R \ closedBall c r ⊆ ball c R
Tactic:
exact diff_subset (ball c R) (closedBall c r)
Proof state after:
no goals
Theorem: Cauchy_formula
Proof state before:
case e_a.e_a
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ (2 * ↑π * I) • y = ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • y
Tactic:
simp only [circleIntegral.integral_smul_const, ne_eq, hr0.ne', not_false_eq_true,
  circleIntegral.integral_sub_center_inv]
Proof state after:
no goals
Theorem: Cauchy_formula
Proof state before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ ‖(∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z) - ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • y‖ =
    ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • (f z - y)‖
Tactic:
simp only [smul_sub]
Proof state after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ ‖(∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z) - ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f c‖ =
    ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z - (z - c)⁻¹ • f c‖
Theorem: Cauchy_formula
Proof state before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ ‖(∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z) - ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f c‖ =
    ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z - (z - c)⁻¹ • f c‖
Tactic:
have hc' : ContinuousOn (fun z => (z - c)⁻¹) (sphere c r) :=
  (continuousOn_id.sub continuousOn_const).inv₀ fun z hz => sub_ne_zero.2 <| hzne _ hz
Proof state after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
hc' : ContinuousOn (fun z => (z - c)⁻¹) (sphere c r)
⊢ ‖(∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z) - ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f c‖ =
    ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z - (z - c)⁻¹ • f c‖
Theorem: Cauchy_formula
Proof state before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
hc' : ContinuousOn (fun z => (z - c)⁻¹) (sphere c r)
⊢ ‖(∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z) - ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f c‖ =
    ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z - (z - c)⁻¹ • f c‖
Tactic:
rw [circleIntegral.integral_sub] <;> refine' (hc'.smul _).circleIntegrable hr0.le
Proof state after:
case hf
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
hc' : ContinuousOn (fun z => (z - c)⁻¹) (sphere c r)
⊢ ContinuousOn (fun x => f x) (sphere c r)

case hg
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
hc' : ContinuousOn (fun z => (z - c)⁻¹) (sphere c r)
⊢ ContinuousOn (fun x => f c) (sphere c r)
Theorem: Cauchy_formula
Proof state before:
case hf
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
hc' : ContinuousOn (fun z => (z - c)⁻¹) (sphere c r)
⊢ ContinuousOn (fun x => f x) (sphere c r)
Tactic:
exact hf.mono <| (sphere_subset_closedBall).trans (closedBall_subset_closedBall hrR)
Proof state after:
no goals
Theorem: Cauchy_formula
Proof state before:
case hg
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
hc' : ContinuousOn (fun z => (z - c)⁻¹) (sphere c r)
⊢ ContinuousOn (fun x => f c) (sphere c r)
Tactic:
exact continuousOn_const
Proof state after:
no goals
Theorem: Cauchy_formula
Proof state before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • (f z - y)‖ ≤ 2 * π * r * (r⁻¹ * (ε / (2 * π)))
Tactic:
refine' circleIntegral.norm_integral_le_of_norm_le_const hr0.le fun z hz => _
Proof state after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
z : ℂ
hz : z ∈ sphere c r
⊢ ‖(z - c)⁻¹ • (f z - y)‖ ≤ r⁻¹ * (ε / (2 * π))
Theorem: Cauchy_formula
Proof state before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
z : ℂ
hz : z ∈ sphere c r
⊢ ‖(z - c)⁻¹ • (f z - y)‖ ≤ r⁻¹ * (ε / (2 * π))
Tactic:
specialize hzne z hz
Proof state after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hz : z ∈ sphere c r
hzne : z ≠ c
⊢ ‖(z - c)⁻¹ • (f z - y)‖ ≤ r⁻¹ * (ε / (2 * π))