Theorem circleAverage_log_norm_sub_const₀

Modification history

2025-09-29 05:27
Mathlib/Analysis/SpecialFunctions/Integrals/PosLogEqCircleAverage.lean
feat: representation of log⁺ as a circle average (#29725) …
Added circleAverage_log_norm_sub_const₀View on Github →