Theorems · Theorem · complex analysis

cauchyPowerSeries_apply

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) (c : ℂ) (R : ℝ) (n : ℕ) (w : ℂ),
  ((cauchyPowerSeries f c R n) fun x => w) =
    (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z

Defined in

Mathlib.MeasureTheory.Integral.CircleIntegral

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace