Theorems · Theorem · complex analysis

ValueDistribution.logCounting_mul_zero_eventuallyLE

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

Asymptotically, 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.

Defined in

Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldProperSpace