Theorems · Definition · complex analysis

ValueDistribution.logCounting

{𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    [ProperSpace 𝕜] → {E : Type u_2} → [inst_2 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (𝕜 → E) → 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, taking multiplicities into account. In the special case where a = ⊤, it counts the poles of f.

Defined in

Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Cited by

45 results in Mathlib

Foundations

Depth 207 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldProperSpaceNormedAddCommGroupNormedSpace