Theorem circleIntegrable_log_norm_sub_const

Modification history

2026-09-17 12:07
Mathlib/Analysis/SpecialFunctions/Integrability/Log.lean
chore: rename files (#42434) …
Modified circleIntegrable_log_norm_sub_constView on Github →
2025-09-29 05:27
Mathlib/Analysis/SpecialFunctions/Integrals/PosLogEqCircleAverage.lean
feat: representation of log⁺ as a circle average (#29725) …
Modified circleIntegrable_log_norm_sub_constView on Github →
2025-07-27 17:59
Mathlib/Analysis/SpecialFunctions/Integrals/PosLogEqCircleAverage.lean
feat: describe posLog in terms of circle averages (#27160) …
Added circleIntegrable_log_norm_sub_constView on Github →