English
Definition of the proximity function: for a meromorphic f and a value a in WithTop E, the proximity measures how well f approximates a on the circle of radius R, with a logarithmic weight. If a = ⊤, it measures how well f approximates infinity.
Русский
Определение функции близости: для мероморфной области f и значения a в WithTop E мера близости оценивает, насколько хорошо f приближает значение a на окружности радиуса R, с логарифмическим весом. Если a = ⊤, она оценивает близость к бесконечности.
LaTeX
$$$\operatorname{proximity}(f,a) = \begin{cases} \operatorname{circleAverage}(\log^+ \|f - a\|^{-1})0, & a \neq \top, \\ \operatorname{circleAverage}(\log^+ \|f\|)0, & a = \top. \end{cases}$$$
Lean4
/-- 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.
-/
noncomputable def proximity : ℝ → ℝ := by
by_cases h : a = ⊤
· exact circleAverage (log⁺ ‖f ·‖) 0
· exact circleAverage (log⁺ ‖f · - a.untop₀‖⁻¹) 0
