Theorems · Theorem · complex analysis

ValueDistribution.proximity_sum_top_le

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {α : Type u_2} (s : Finset α) (f : α → ℂ → E),
  (∀ a ∈ s, Meromorphic (f a)) →
    ValueDistribution.proximity (∑ a ∈ s, f a) ⊤ ≤
      ∑ a ∈ s, ValueDistribution.proximity (f a) ⊤ + fun x => Real.log ↑s.card

The proximity function of a sum of functions at ⊤ is less than or equal to the sum of the proximity functions of the summand, plus log of the number of summands.

Defined in

Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace