Theorem circleAverage_log_norm_sub_const_of_mem_closedBall

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_of_mem_closedBallView on Github →