Theorems · Definition · complex analysis

ValueDistribution.proximity

{E : Type u_1} → [NormedAddCommGroup E] → (ℂ → E) → WithTop E → ℝ → ℝ

The Proximity Function of Value Distribution Theory If f : ℂ → E is meromorphic and a : WithTop E is any value, the proximity function is a logarithmically weighted measure quantifying how well a meromorphic function f approximates the constant function a on the circle of radius R in the complex plane. In the special case where a = ⊤, it quantifies how well f approximates infinity.

Defined in

Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Cited by

28 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroup