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.

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.

TODO

Establish the analogous characterization of meromorphic functions with finite set of poles, as functions whose logarithmic counting function is big-O of log.

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.

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.