Theorem Real.Continuous.circleAverage

Modification history

2026-05-20 04:59
Mathlib/MeasureTheory/Integral/CircleAverage.lean
feat: simple lemmas on circle integrability (#39566) …
Added Real.Continuous.circleAverageView on Github →