English
The Cauchy formula for the derivative of a holomorphic function: the derivative at a point equals a certain circle integral involving f.
Русский
Формула Коши для производной голоморфной функции: производная в точке равна определенному круговому интегралу, зависящему от f.
LaTeX
$$$\displaystyle \frac{1}{2\pi i} \oint_{|z-c|=R} \frac{f(z)}{(z-c)^2} \,dz = f'(c).$$$
Lean4
/-- The Cauchy formula for the derivative of a holomorphic function. -/
theorem two_pi_I_inv_smul_circleIntegral_sub_sq_inv_smul_of_differentiable {U : Set ℂ} (hU : IsOpen U) {c w₀ : ℂ}
{R : ℝ} {f : ℂ → E} (hc : closedBall c R ⊆ U) (hf : DifferentiableOn ℂ f U) (hw₀ : w₀ ∈ ball c R) :
((2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = deriv f w₀ := by
-- We apply the removable singularity theorem and the Cauchy formula to `dslope f w₀`
have hf' : DifferentiableOn ℂ (dslope f w₀) U :=
(differentiableOn_dslope (hU.mem_nhds ((ball_subset_closedBall.trans hc) hw₀))).mpr hf
have h0 := (hf'.diffContOnCl_ball hc).two_pi_i_inv_smul_circleIntegral_sub_inv_smul hw₀
rw [← dslope_same, ← h0]
congr 1
trans ∮ z in C(c, R), ((z - w₀) ^ 2)⁻¹ • (f z - f w₀)
· have h1 : ContinuousOn (fun z : ℂ => ((z - w₀) ^ 2)⁻¹) (sphere c R) :=
by
refine ((continuous_id'.sub continuous_const).pow 2).continuousOn.inv₀ fun w hw h => ?_
exact sphere_disjoint_ball.ne_of_mem hw hw₀ (sub_eq_zero.mp (sq_eq_zero_iff.mp h))
have h2 : CircleIntegrable (fun z : ℂ => ((z - w₀) ^ 2)⁻¹ • f z) c R :=
by
refine ContinuousOn.circleIntegrable (pos_of_mem_ball hw₀).le ?_
exact h1.smul (hf.continuousOn.mono (sphere_subset_closedBall.trans hc))
have h3 : CircleIntegrable (fun z : ℂ => ((z - w₀) ^ 2)⁻¹ • f w₀) c R :=
ContinuousOn.circleIntegrable (pos_of_mem_ball hw₀).le (h1.smul continuousOn_const)
have h4 : (∮ z : ℂ in C(c, R), ((z - w₀) ^ 2)⁻¹) = 0 := by
simpa using circleIntegral.integral_sub_zpow_of_ne (by decide : (-2 : ℤ) ≠ -1) c w₀ R
simp only [smul_sub, circleIntegral.integral_sub h2 h3, h4, circleIntegral.integral_smul_const, zero_smul, sub_zero]
· refine circleIntegral.integral_congr (pos_of_mem_ball hw₀).le fun z hz => ?_
simp only [dslope_of_ne, Metric.sphere_disjoint_ball.ne_of_mem hz hw₀, slope, ← smul_assoc, sq, mul_inv, Ne,
not_false_iff, vsub_eq_sub, Algebra.id.smul_eq_mul]
