Commit 2026-01-06 18:25 0b1935a1

View on Github →

feat: use new predicate Meromorphic in Value Distribution Theory (#33231) Following a discussion of Zulip, port the matlib section on Value Distribution Theory to use the new predicate Meromorphic. #mathlib4 > Introducing Meromorphic @ 💬

Estimated changes

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

modified theorem ValueDistribution.characteristic_pow_top

modified theorem ValueDistribution.characteristic_pow_zero

modified theorem ValueDistribution.characteristic_sub_characteristic_eq_proximity_sub_proximity

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

modified theorem Function.locallyFinsuppWithin.toClosedBall_divisor

modified theorem ValueDistribution.logCounting_add_analyticOn

modified theorem ValueDistribution.logCounting_add_const

modified theorem ValueDistribution.logCounting_add_top_eventuallyLE

modified theorem ValueDistribution.logCounting_add_top_le

modified theorem ValueDistribution.logCounting_pow_top

modified theorem ValueDistribution.logCounting_pow_zero

modified theorem ValueDistribution.logCounting_sub_const

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

modified theorem ValueDistribution.abs_characteristic_sub_characteristic_shift_le

modified theorem ValueDistribution.characteristic_sub_characteristic_inv

modified theorem ValueDistribution.characteristic_sub_characteristic_inv_at_zero

modified theorem ValueDistribution.characteristic_sub_characteristic_inv_le

modified theorem ValueDistribution.isBigO_characteristic_sub_characteristic_inv

modified theorem ValueDistribution.isBigO_characteristic_sub_characteristic_shift

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

modified theorem ValueDistribution.proximity_add_top_le

modified theorem ValueDistribution.proximity_mul_top_le

modified theorem ValueDistribution.proximity_mul_zero_le

modified theorem ValueDistribution.proximity_sub_proximity_inv_eq_circleAverage