Commit 2025-05-01 08:53 ce779357

View on Github →

feat: add logarithmic counting function of Value Distribution Theory (#23627) Implement the logarithmic counting function of Value Distribution Theory and provide supporting API. This material is used in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.

Estimated changes

Modified Mathlib.lean

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

added theorem Function.locallyFinsuppWithin.logCounting_eval_zero

added theorem ValueDistribution.logCounting_add_analyticOn

added theorem ValueDistribution.logCounting_add_const

added theorem ValueDistribution.logCounting_coe

added theorem ValueDistribution.logCounting_coe_eq_logCounting_sub_const_zero

added theorem ValueDistribution.logCounting_eval_zero

added theorem ValueDistribution.logCounting_inv

added theorem ValueDistribution.logCounting_sub_const

added theorem ValueDistribution.logCounting_top

added theorem ValueDistribution.logCounting_zero

added theorem ValueDistribution.log_counting_zero_sub_logCounting_top