English
An auxiliary lemma for the circle integral sub_inv_smul formula; under suitable hypotheses the integral equals (2πi) f(w).
Русский
Вспомогательная лемма для формулы circle integral sub_inv_smul; при подходящих предпосылках интеграл равен (2πi) f(w).
LaTeX
$$$\\oint_{z\\in C(c,R)} (z-w)^{-1} \\cdot f(z) \\, dz = (2 \\pi i) \\cdot f(w)$$$
Lean4
/-- **Cauchy integral formula**: if `f : ℂ → E` is complex differentiable on an open disc and is
continuous on its closure, then for any `w` in this open ball we have
$\frac{1}{2πi}\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=f(w)$. -/
theorem _root_.DiffContOnCl.two_pi_i_inv_smul_circleIntegral_sub_inv_smul {R : ℝ} {c w : ℂ} {f : ℂ → E}
(hf : DiffContOnCl ℂ f (ball c R)) (hw : w ∈ ball c R) :
((2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z) = f w :=
by
have hR : 0 < R := not_le.mp (ball_eq_empty.not.mp (Set.nonempty_of_mem hw).ne_empty)
refine two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable countable_empty hw ?_ ?_
· simpa only [closure_ball c hR.ne.symm] using hf.continuousOn
· simpa only [diff_empty] using fun z hz => hf.differentiableAt isOpen_ball hz
