Theorems · Theorem · complex analysis

hasFPowerSeriesOn_cauchy_integral

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R : NNReal},
  CircleIntegrable f c ↑R →
    0 < R →
      HasFPowerSeriesOnBall (fun w => (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - w)⁻¹ • f z)
        (cauchyPowerSeries f c ↑R) c ↑R

For any circle integrable function f, the power series cauchyPowerSeries f c R, R > 0, converges to the Cauchy integral (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z on the open disc Metric.ball c R.

Defined in

Mathlib.MeasureTheory.Integral.CircleIntegral

Cited by

2 results in Mathlib

Foundations

Depth 259 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace