English
If f is continuous on a closed disk of radius R about c and differentiable off a countable interior set, then (1/(2πi)) times the circle integral of (z − w)^{-1} f(z) equals f(w) for w in the disk.
Русский
Пусть f непрерывна на закрытом диске радиуса R вокруг c и дифференцируема вне счётного множества внутри; тогда (1/(2πi)) раз circle integral от (z − w)^{-1} f(z) dz равен f(w) для w внутри диска.
LaTeX
$$$\\frac{1}{2\\pi i} \\oint_{|z-c|=R} (z-w)^{-1} \\cdot f(z) \\, dz = f(w)$$$
Lean4
/-- **Cauchy integral formula**: if `f : ℂ → E` is continuous on a closed disc of radius `R` and is
complex differentiable at all but countably many points of its interior, then for any `w` in this
interior we have $\frac{1}{2πi}\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=f(w)$.
-/
theorem two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable {R : ℝ} {c w : ℂ} {f : ℂ → E}
{s : Set ℂ} (hs : s.Countable) (hw : w ∈ ball c R) (hc : ContinuousOn f (closedBall c R))
(hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x) : ((2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z) = f w :=
by
have hR : 0 < R := dist_nonneg.trans_lt hw
suffices w ∈ closure (ball c R \ s) by
lift R to ℝ≥0 using hR.le
have A : ContinuousAt (fun w => (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z) w :=
by
have := hasFPowerSeriesOn_cauchy_integral ((hc.mono sphere_subset_closedBall).circleIntegrable R.coe_nonneg) hR
refine this.continuousOn.continuousAt (EMetric.isOpen_ball.mem_nhds ?_)
rwa [Metric.emetric_ball_nnreal]
have B : ContinuousAt f w := hc.continuousAt (closedBall_mem_nhds_of_mem hw)
refine tendsto_nhds_unique_of_frequently_eq A B ((mem_closure_iff_frequently.1 this).mono ?_)
intro z hz
rw [circleIntegral_sub_inv_smul_of_differentiable_on_off_countable_aux hs hz hc hd, inv_smul_smul₀]
simp [Real.pi_ne_zero, I_ne_zero]
refine
mem_closure_iff_nhds.2 fun t ht =>
?_
-- TODO: generalize to any vector space over `ℝ`
set g : ℝ → ℂ := fun x => w + ofReal x
have : Tendsto g (𝓝 0) (𝓝 w) := (continuous_const.add continuous_ofReal).tendsto' 0 w (add_zero _)
rcases mem_nhds_iff_exists_Ioo_subset.1 (this <| inter_mem ht <| isOpen_ball.mem_nhds hw) with ⟨l, u, hlu₀, hlu_sub⟩
obtain ⟨x, hx⟩ : (Ioo l u \ g ⁻¹' s).Nonempty :=
by
refine diff_nonempty.2 fun hsub => ?_
have : (Ioo l u).Countable := (hs.preimage ((add_right_injective w).comp ofReal_injective)).mono hsub
rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioo_real (hlu₀.1.trans hlu₀.2)] at this
exact this.not_gt Cardinal.aleph0_lt_continuum
exact ⟨g x, (hlu_sub hx.1).1, (hlu_sub hx.1).2, hx.2⟩
