Commit 2026-09-17 12:07 067a2c89

View on Github →

chore: rename files (#42434) Rename files in Mathlib/Analysis/SpecialFunctions/Integrability and Mathlib/Analysis/SpecialFunctions/Integrals to better reflect their contents, and update docstrings. The current file names are somewhat unsystematic, very specialized, and will be seen as misleading once more material is added.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Complex/JensenFormula.lean

Modified Mathlib/Analysis/Complex/ValueDistribution/Proximity/Basic.lean

Modified Mathlib/Analysis/Complex/ValueDistribution/Proximity/IntegralPresentation.lean

Modified Mathlib/Analysis/Polynomial/MahlerMeasure.lean

Renamed Mathlib/Analysis/SpecialFunctions/Integrability/LogMeromorphic.lean to Mathlib/Analysis/SpecialFunctions/Integrability/Log.lean

deleted theorem MeromorphicOn.circleIntegrable_posLog_norm

deleted theorem MeromorphicOn.circleIntegrable_posLog_norm_of_nonneg

deleted theorem MeromorphicOn.intervalIntegrable_posLog_norm

added theorem circleIntegrable_log_norm_sub_const

Created Mathlib/Analysis/SpecialFunctions/Integrability/PosLog.lean

added theorem MeromorphicOn.circleIntegrable_posLog_norm

added theorem MeromorphicOn.circleIntegrable_posLog_norm_of_nonneg

added theorem MeromorphicOn.intervalIntegrable_posLog_norm

Renamed Mathlib/Analysis/SpecialFunctions/Integrals/LogTrigonometric.lean to Mathlib/Analysis/SpecialFunctions/Integrals/Log.lean

Renamed Mathlib/Analysis/SpecialFunctions/Integrals/PosLogEqCircleAverage.lean to Mathlib/Analysis/SpecialFunctions/Integrals/PosLog.lean

deleted theorem circleIntegrable_log_norm_sub_const