Theorems · Theorem · measure theory

Real.circleAverage_mono_on_of_le_circle

∀ {c : ℂ} {R : ℝ} {f : ℂ → ℝ} {a : ℝ},
  CircleIntegrable f c R → (∀ x ∈ Metric.sphere c |R|, f x ≤ a) → Real.circleAverage f c R ≤ a

If f x is smaller than a on for every point of the circle, then the circle average of f is smaller than a.

Defined in

Mathlib.MeasureTheory.Integral.CircleAverage

Cited by

2 results in Mathlib

Foundations

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