Theorems · Theorem · measure theory

Real.ContinuousOn.circleAverage

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℂ → E} {s : Set ℝ} {c : ℂ},
  ContinuousOn f {z | ‖z - c‖ ∈ s} → (∀ r ∈ s, 0 ≤ r) → ContinuousOn (Real.circleAverage f c) s

The circle average of a continuous function is itself continuous, as a function of the radius.

Defined in

Mathlib.MeasureTheory.Integral.CircleAverage

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace