Theorems · Theorem · complex analysis

circleIntegral.norm_integral_lt_of_norm_le_const_of_lt

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R C : ℝ},
  0 < R →
    ContinuousOn f (Metric.sphere c R) →
      (∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C) →
        (∃ z ∈ Metric.sphere c R, ‖f z‖ < C) → ‖∮ (z : ℂ) in C(c, R), f z‖ < 2 * Real.pi * R * C

If f is continuous on the circle |z - c| = R, R > 0, the ‖f z‖ is less than or equal to C : ℝ on this circle, and this norm is strictly less than C at some point z of the circle, then ‖∮ z in C(c, R), f z‖ < 2 * π * R * C.

Defined in

Mathlib.MeasureTheory.Integral.CircleIntegral

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace