Theorems · Theorem · complex analysis

hasSum_two_pi_I_cauchyPowerSeries_integral

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R : ℝ} {w : ℂ},
  CircleIntegrable f c R →
    ‖w‖ < R →
      HasSum (fun n => ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
        (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)

For any circle integrable function f, the power series cauchyPowerSeries f c R multiplied by 2πI converges to the integral ∮ 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 257 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace