Commit 2026-01-28 06:03 65ada599

View on Github →

feat: add simple congruence lemmata for meromorphicity and value distribution theory (#34302) Add simple congruence lemmas for meromorphicity and the main functions of Value Distribution Theory. Remove unnecessary assumption from divisor_congr_codiscreteWithin. Minor golfing.

Estimated changes

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

added theorem ValueDistribution.characteristic_congr_codiscrete

modified theorem ValueDistribution.characteristic_even

modified theorem ValueDistribution.characteristic_eventually_nonneg

modified theorem ValueDistribution.characteristic_nonneg

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

added theorem ValueDistribution.logCounting_congr_codiscrete

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

added theorem ValueDistribution.proximity_congr_codiscrete

added theorem ValueDistribution.proximity_congr_codiscreteWithin

added theorem ValueDistribution.proximity_const

Modified Mathlib/Analysis/Meromorphic/Basic.lean

added theorem Meromorphic.congr_codiscrete

added theorem meromorphicOn_congr_codiscreteWithin

added theorem meromorphic_congr_codiscrete

Modified Mathlib/Analysis/Meromorphic/Divisor.lean

modified theorem MeromorphicOn.divisor_congr_codiscreteWithin