Theorems · Theorem · complex analysis

ValueDistribution.circleAverage_circleAverage_eq_proximity_top

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

Presentation of the proximity function as iterated circle averages.

Defined in

Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Cited by

1 results in Mathlib

Foundations

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