Theorems · Theorem · complex analysis

ValueDistribution.logCounting_mul_zero_le

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {f₁ f₂ : 𝕜 → 𝕜} {r : ℝ},
  1 ≤ r →
    Meromorphic f₁ →
      (∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤) →
        Meromorphic f₂ →
          (∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤) →
            ValueDistribution.logCounting (f₁ * f₂) 0 r ≤
              (ValueDistribution.logCounting f₁ 0 + ValueDistribution.logCounting f₂ 0) r

For 1 ≤ r, the logarithmic counting function for the zeros of f * g is less than or equal to the sum of the logarithmic counting functions for the zeros of f and g, respectively. Note: The statement proven here is found at the top of page 169 of [Lang: Introduction to Complex Hyperbolic Spaces](https://link.springer.com/book/10.1007/978-1-4757-1945-1) where it is written as an inequality between functions. This could be interpreted as claiming that the inequality holds for ALL values of r, which is not true. For a counterexample, take f₁ : z → z and f₂ : z → z⁻¹. Then, - logCounting f₁ 0 = log - logCounting f₂ 0 = 0 - logCounting (f₁ * f₂) 0 = 0 But log r is negative for small r.

Defined in

Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldProperSpace