Commit 2026-04-04 15:31 6e9a872b

View on Github →

chore(Analysis/SpecialFunctions/Integrability): better theorem names in LogMeromorphic.lean (#37308) Put MeromorphicOn first in names as suggested by @j-loreaux in review of #36950. This is the correct Mathlib naming and makes applications simpler.

Estimated changes

Modified Mathlib/Analysis/Complex/JensenFormula.lean

Modified Mathlib/Analysis/Complex/ValueDistribution/FirstMainTheorem.lean

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

Modified Mathlib/Analysis/Polynomial/MahlerMeasure.lean

Modified Mathlib/Analysis/SpecialFunctions/Integrability/LogMeromorphic.lean

added theorem MeromorphicOn.circleIntegrable_log_norm

added theorem MeromorphicOn.circleIntegrable_log_norm_of_nonneg

added theorem MeromorphicOn.circleIntegrable_posLog_norm

added theorem MeromorphicOn.circleIntegrable_posLog_norm_of_nonneg

added theorem MeromorphicOn.intervalIntegrable_log_norm

added theorem MeromorphicOn.intervalIntegrable_posLog_norm

deleted theorem circleIntegrable_log_norm_meromorphicOn

deleted theorem circleIntegrable_log_norm_meromorphicOn_of_nonneg

deleted theorem circleIntegrable_posLog_norm_meromorphicOn

deleted theorem circleIntegrable_posLog_norm_meromorphicOn_of_nonneg

deleted theorem intervalIntegrable_log_norm_meromorphicOn

deleted theorem intervalIntegrable_posLog_norm_meromorphicOn

Modified Mathlib/Analysis/SpecialFunctions/Integrals/PosLogEqCircleAverage.lean