Theorems · Theorem · complex analysis

ValueDistribution.proximity_sub_proximity_inv_eq_circleAverage

∀ {f : ℂ → ℂ},
  Meromorphic f →
    ValueDistribution.proximity f ⊤ - ValueDistribution.proximity f⁻¹ ⊤ = Real.circleAverage (fun x => Real.log ‖f x‖) 0

For complex-valued f, the difference between proximity f ⊤ and proximity f⁻¹ ⊤ is the circle average of log ‖f ·‖.

Defined in

Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Cited by

1 results in Mathlib

Foundations

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