Theorems · Theorem · complex analysis

ValueDistribution.characteristic_mul_top_le

∀ {f₁ f₂ : ℂ → ℂ} {r : ℝ},
  1 ≤ r →
    Meromorphic f₁ →
      (∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤) →
        Meromorphic f₂ →
          (∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤) →
            ValueDistribution.characteristic (f₁ * f₂) ⊤ r ≤
              (ValueDistribution.characteristic f₁ ⊤ + ValueDistribution.characteristic f₂ ⊤) r

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

Defined in

Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Cited by

1 results in Mathlib

Foundations

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