Theorem Real.circleAverage_fun_add

Modification history

2025-11-24 08:57
Mathlib/MeasureTheory/Integral/CircleAverage.lean
feat: behavior of the proximity function under addition (#31556) …
Modified Real.circleAverage_fun_addView on Github →
2025-05-09 13:13
Mathlib/MeasureTheory/Integral/CircleAverage.lean
feat: add circle averages (#24427) …
Added Real.circleAverage_fun_addView on Github →