Commit 2025-12-11 19:40 da367fd9

View on Github →

chore: uniformize theorem naming (#32726) Following a suggestion made by @j-loreaux in the review of an earlier PR, rename several of the theorems introduced lately in Mathlib/Analysis/Complex/ValueDistribution/*.

Estimated changes

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

added theorem ValueDistribution.characteristic_mul_top_eventuallyLE

added theorem ValueDistribution.characteristic_mul_top_le

added theorem ValueDistribution.characteristic_mul_zero_eventuallyLE

added theorem ValueDistribution.characteristic_mul_zero_le

deleted theorem ValueDistribution.characteristic_top_mul_eventually_le

deleted theorem ValueDistribution.characteristic_top_mul_le

deleted theorem ValueDistribution.characteristic_zero_mul_eventually_le

deleted theorem ValueDistribution.characteristic_zero_mul_le

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

added theorem Function.locallyFinsuppWithin.logCounting_eventuallyLE

deleted theorem Function.locallyFinsuppWithin.logCounting_eventually_le

added theorem ValueDistribution.logCounting_mul_top_eventuallyLE

added theorem ValueDistribution.logCounting_mul_top_le

added theorem ValueDistribution.logCounting_mul_zero_eventuallyLE

added theorem ValueDistribution.logCounting_mul_zero_le

deleted theorem ValueDistribution.logCounting_top_mul_eventually_le

deleted theorem ValueDistribution.logCounting_top_mul_le

deleted theorem ValueDistribution.logCounting_zero_mul_eventually_le

deleted theorem ValueDistribution.logCounting_zero_mul_le

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

added theorem ValueDistribution.proximity_mul_top_le

added theorem ValueDistribution.proximity_mul_zero_le

deleted theorem ValueDistribution.proximity_top_mul_le

deleted theorem ValueDistribution.proximity_zero_mul_le