Asymptotic Behavior of the Logarithmic Counting Function

If f is meromorphic over a field 𝕜, we show that the logarithmic counting function for the poles of f is asymptotically bounded if and only if f has only removable singularities. See Page 170f of Lang, Introduction to Complex Hyperbolic Spaces for a detailed discussion.

Analogously, characterize meromorphic functions with finite set of poles, as functions whose logarithmic counting function is big-O of log.

Implementation Notes

We establish the result first for the logarithmic counting function for functions with locally finite support on 𝕜 and then specialize to the setting where the function with locally finite support is the pole or zero-divisor of a meromorphic function.

Logarithmic Counting Functions for Functions with Locally Finite Support

theorem Function.locallyFinsuppWithin.one_isLittleO_logCounting_single {E : Type u_1} [NormedAddCommGroup E] [DecidableEq E] [ProperSpace E] {e : E} : 1 =o[Filter.atTop] logCounting (single e 1)

Qualitative consequence of logCounting_single_eq_log_sub_const. The constant function 1 : ℝ → ℝ is little o of the logarithmic counting function attached to single e.

theorem Function.locallyFinsuppWithin.zero_iff_logCounting_bounded {E : Type u_1} [NormedAddCommGroup E] [ProperSpace E] {D : locallyFinsuppWithin Set.univ ℤ} (h : 0 ≤ D) : D = 0 ↔ logCounting D =O[Filter.atTop] 1

A non-negative function with locally finite support is zero if and only if its logarithmic counting functions is asymptotically bounded.

theorem Function.locallyFinsuppWithin.logCounting_single_isBigO_log {E : Type u_1} [NormedAddCommGroup E] [DecidableEq E] [ProperSpace E] {e : E} {n : ℤ} : logCounting (single e n) =O[Filter.atTop] Real.log

The logarithmic counting function of a singleton is big-O of log. This is the qualitative consequence of logCounting_single_eq_log_sub_const.

theorem Function.locallyFinsuppWithin.logCounting_isBigO_log_of_finite_support {E : Type u_1} [NormedAddCommGroup E] [ProperSpace E] {D : locallyFinsupp E ℤ} (h : (support D).Finite) : logCounting D =O[Filter.atTop] Real.log

A function with finite support has a logarithmic counting function that is big-O of log.

theorem Function.locallyFinsuppWithin.finite_support_of_logCounting_isBigO_log {E : Type u_1} [NormedAddCommGroup E] [ProperSpace E] {D : locallyFinsupp E ℤ} (h : 0 ≤ D) (hO : logCounting D =O[Filter.atTop] Real.log) : (support D).Finite

A non-negative function whose logarithmic counting function is big-O of log has finite support.

theorem Function.locallyFinsuppWithin.finite_support_iff_logCounting_isBigO_log {E : Type u_1} [NormedAddCommGroup E] [ProperSpace E] {D : locallyFinsupp E ℤ} (h : 0 ≤ D) : (support D).Finite ↔ logCounting D =O[Filter.atTop] Real.log

A non-negative function with locally finite support has finite support if and only if its logarithmic counting function is big-O of log.

Logarithmic Counting Functions for the Poles of a Meromorphic Function

theorem ValueDistribution.logCounting_isBigO_one_iff_analyticOnNhd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} (h : Meromorphic f) : logCounting f ⊤ =O[Filter.atTop] 1 ↔ AnalyticOnNhd 𝕜 (toMeromorphicNFOn f Set.univ) Set.univ

A meromorphic function has only removable singularities if and only if the logarithmic counting function for its pole divisor is asymptotically bounded.

theorem ValueDistribution.logCounting_isBigO_log_iff_finite_support {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} : logCounting f ⊤ =O[Filter.atTop] Real.log ↔ (MeromorphicOn.divisor f Set.univ)⁻.support.Finite

A meromorphic function has a finite set of poles if and only if the logarithmic counting function for its pole-divisor is big-O of log.