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