Theorem circleAverage_log_norm_sub_const₁

Modification history

2025-07-27 17:59
Mathlib/Analysis/SpecialFunctions/Integrals/PosLogEqCircleAverage.lean
feat: describe posLog in terms of circle averages (#27160) …
Added circleAverage_log_norm_sub_const₁View on Github →