Documentation

Mathlib.Analysis.Complex.ValueDistribution.CountingFunction

The Counting Function of Value Distribution Theory #

For nontrivially normed fields ๐•œ, this file defines the logarithmic counting function of a meromorphic function defined on ๐•œ. Also known as the Nevanlinna counting function, this is one of the three main functions used in Value Distribution Theory.

The counting function of a meromorphic function f is a logarithmically weighted measure of the number of times the function f takes a given value a within the disk โˆฃzโˆฃ โ‰ค r, counting multiplicities. See SectionVI.1 of Lang: Introduction to Complex Hyperbolic Spaces or Section1.1 of Noguchi-Winkelmann: Nevanlinna Theory in Several Complex Variables and Diophantine Approximation for a detailed discussion.

Implementation Notes #

TODO #

Supporting Notation #

Shorthand notation for the restriction of a function with locally finite support within Set.univ to the closed unit ball of radius r.

Equations
Instances For

    The Logarithmic Counting Function of a Function with Locally Finite Support #

    Definition of the logarithmic counting function, as a group morphism mapping functions D with locally finite support to maps โ„ โ†’ โ„. Given D, the result map logCounting D takes a real r : โ„ to a logarithmically weighted measure of values that D takes within the disk โˆฃzโˆฃ โ‰ค r.

    Implementation Note: In case where z = 0, the term log (r * โ€–zโ€–โปยน) evaluates to zero, which is typically different from log r - log โ€–zโ€– = log r. The summand (D 0) * log r compensates this, producing cleaner formulas when the logarithmic counting function is used in the main theorms of Value Distribution Theory. We refer the reader to page 164 of Lang: Introduction to Complex Hyperbolic Spaces for more details.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]

      Evaluation of the logarithmic counting function at zero yields zero.

      The Logarithmic Counting Function of a Meromorphic Function #

      noncomputable def ValueDistribution.logCounting {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] [ProperSpace ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] (f : ๐•œ โ†’ E) (a : WithTop E) :

      The logarithmic counting function of a meromorphic function.

      If f : ๐•œ โ†’ E is meromorphic and a : WithTop E is any value, this is a logarithmically weighted measure of the number of times the function f takes a given value a within the disk โˆฃzโˆฃ โ‰ค r, counting multiplicities. In the special case where a = โŠค, it counts the poles of f.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem ValueDistribution.logCounting_coe {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] [ProperSpace ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {aโ‚€ : E} :
        logCounting f โ†‘aโ‚€ = Function.locallyFinsuppWithin.logCounting (MeromorphicOn.divisor (fun (z : ๐•œ) => f z - aโ‚€) Set.univ)โบ

        For finite values aโ‚€, the logarithmic counting function logCounting f aโ‚€ is the counting function associated with the zero-divisor of the meromorphic function f - aโ‚€.

        theorem ValueDistribution.logCounting_coe_eq_logCounting_sub_const_zero {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] [ProperSpace ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {aโ‚€ : E} :
        logCounting f โ†‘aโ‚€ = logCounting (f - fun (x : ๐•œ) => aโ‚€) 0

        For finite values aโ‚€, the logarithmic counting function logCounting f aโ‚€ equals the logarithmic counting function for the value zero of the shifted function f - aโ‚€.

        The logarithmic counting function logCounting f 0 is the counting function associated with the zero-divisor of f.

        The logarithmic counting function logCounting f โŠค is the counting function associated with the pole-divisor of f.

        @[simp]
        theorem ValueDistribution.logCounting_eval_zero {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] [ProperSpace ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {a : WithTop E} :
        logCounting f a 0 = 0

        Evaluation of the logarithmic counting function at zero yields zero.

        The counting function associated with the divisor of f is the difference between logCounting f 0 and logCounting f โŠค.

        Elementary Properties of the Counting Function #

        @[simp]
        theorem ValueDistribution.logCounting_inv {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] [ProperSpace ๐•œ] {f : ๐•œ โ†’ ๐•œ} :

        Relation between the logarithmic counting function of f and of fโปยน.

        theorem ValueDistribution.logCounting_add_analyticOn {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] [ProperSpace ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f g : ๐•œ โ†’ E} (hf : MeromorphicOn f Set.univ) (hg : AnalyticOn ๐•œ g Set.univ) :

        Adding an analytic function does not change the counting function counting poles.

        @[simp]
        theorem ValueDistribution.logCounting_add_const {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] [ProperSpace ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {aโ‚€ : E} (hf : MeromorphicOn f Set.univ) :
        logCounting (f + fun (x : ๐•œ) => aโ‚€) โŠค = logCounting f โŠค

        Special case of logCounting_add_analyticOn: Adding a constant does not change the counting function counting poles.

        @[simp]
        theorem ValueDistribution.logCounting_sub_const {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] [ProperSpace ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {aโ‚€ : E} (hf : MeromorphicOn f Set.univ) :
        logCounting (f - fun (x : ๐•œ) => aโ‚€) โŠค = logCounting f โŠค

        Special case of logCounting_add_analyticOn: Subtracting a constant does not change the counting function counting poles.