Theorems · Theorem · complex analysis

CircleIntegrable.out

∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℂ → E} {c : ℂ} {R : ℝ} [inst_1 : NormedSpace ℂ E],
  CircleIntegrable f c R →
    IntervalIntegrable (fun θ => deriv (circleMap c R) θ • f (circleMap c R θ)) MeasureTheory.volume 0 (2 * Real.pi)

The function we actually integrate over [0, 2π] in the definition of circleIntegral is integrable.

Defined in

Mathlib.MeasureTheory.Integral.CircleIntegral

Cited by

5 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace