Theorems · Theorem · complex analysis

ValueDistribution.logCounting_mul_top_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₂) ⊤ r ≤
              (ValueDistribution.logCounting f₁ ⊤ + ValueDistribution.logCounting f₂ ⊤) r

For 1 ≤ r, the logarithmic counting function for the poles of f * g is less than or equal to the sum of the logarithmic counting functions for the poles of f and g, respectively.

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