Documentation

Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Truncated

Truncated Divisors and Truncated Counting Functions #

This file introduces (and provides API for) the Truncated Logarithmic Counting Functions. These differ from the Logarithmic Counting Function in that they disregard pole orders, and count all poles with multiplicity one.

The truncated counting function is the quantity through which the Second Main Theorem of Value Distribution Theory is classically stated.

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

source
theorem Function.locallyFinsuppWithin.logCounting_truncate_le {E : Type u_1} [NormedAddCommGroup E] [ProperSpace E] (D : locallyFinsupp E ℤ) {r : ℝ} (hr : 1 ≤ r) :
logCounting (truncate₁ D) r ≤ logCounting D r

For 1 ≤ r, the counting function of a truncated divisor is bounded above by the counting function of the divisor itself.

source
theorem Function.locallyFinsuppWithin.logCounting_truncate_nonneg {E : Type u_1} [NormedAddCommGroup E] [ProperSpace E] {D : locallyFinsupp E ℤ} (h : 0 ≤ D) {r : ℝ} (hr : 1 ≤ r) :
0 ≤ logCounting (truncate₁ D) r

For 1 ≤ r, the counting function of a truncated non-negative divisor is non-negative.

The Truncated Logarithmic Counting Function of a Meromorphic Function #

source
noncomputable def ValueDistribution.truncatedLogCounting {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 → E) (a : WithTop E) :
ℝ → ℝ

The truncated logarithmic counting function of Value Distribution Theory: like logCounting f a, but counting each zero/pole once, regardless of multiplicity. In the special case where a = ⊤, it counts the poles of f, each with multiplicity one.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem ValueDistribution.truncatedLogCounting_top {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} :
    truncatedLogCounting f ⊤ = Function.locallyFinsuppWithin.logCounting (MeromorphicOn.divisor f Set.univ)⁻.truncate₁

    The truncated logarithmic counting function truncatedLogCounting f ⊤ counts the poles of f, each with multiplicity one.

    source
    theorem ValueDistribution.truncatedLogCounting_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a₀ : E} :
    truncatedLogCounting f ↑a₀ = Function.locallyFinsuppWithin.logCounting (MeromorphicOn.divisor (fun (x : 𝕜) => f x - a₀) Set.univ)⁺.truncate₁

    For finite values a₀, the truncated logarithmic counting function truncatedLogCounting f a₀ counts the zeros of f - a₀, each with multiplicity one.

    source
    theorem ValueDistribution.truncatedLogCounting_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} :
    truncatedLogCounting f 0 = Function.locallyFinsuppWithin.logCounting (MeromorphicOn.divisor f Set.univ)⁺.truncate₁

    The truncated logarithmic counting function truncatedLogCounting f 0 counts the zeros of f, each with multiplicity one.

    source
    @[simp]
    theorem ValueDistribution.truncatedLogCounting_eval_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a : WithTop E} :
    truncatedLogCounting f a 0 = 0

    Evaluation of the truncated logarithmic counting function at zero yields zero.

    source
    theorem ValueDistribution.truncatedLogCounting_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a : WithTop E} {r : ℝ} (hr : 1 ≤ r) :
    truncatedLogCounting f a r ≤ logCounting f a r

    For 1 ≤ r, the truncated logarithmic counting function is bounded above by the ordinary logarithmic counting function.

    source
    theorem ValueDistribution.truncatedLogCounting_nonneg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a : WithTop E} {r : ℝ} (hr : 1 ≤ r) :
    0 ≤ truncatedLogCounting f a r

    For 1 ≤ r, the truncated logarithmic counting function is non-negative.

    source
    theorem ValueDistribution.truncatedLogCounting_monotoneOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a : WithTop E} :
    MonotoneOn (truncatedLogCounting f a) (Set.Ioi 0)

    The truncated logarithmic counting function is monotonous.

    source
    @[simp]
    theorem ValueDistribution.truncatedLogCounting_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {f : 𝕜 → 𝕜} :
    truncatedLogCounting f⁻¹ ⊤ = truncatedLogCounting f 0

    Relation between the truncated logarithmic counting functions of f and of f⁻¹.

    source
    theorem ValueDistribution.truncatedLogCounting_congr_codiscrete {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} (hfg : f =ᶠ[Filter.codiscrete ℂ] g) :
    truncatedLogCounting f = truncatedLogCounting g

    If two functions differ only on a discrete set, then their truncated logarithmic counting functions agree.