Theorems · Theorem · complex analysis

norm_cauchyPowerSeries_le

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) (c : ℂ) (R : ℝ) (n : ℕ),
  ‖cauchyPowerSeries f c R n‖ ≤ ((2 * Real.pi)⁻¹ * ∫ (θ : ℝ) in 0..2 * Real.pi, ‖f (circleMap c R θ)‖) * |R|⁻¹ ^ n

Defined in

Mathlib.MeasureTheory.Integral.CircleIntegral

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace