English
The characteristic function of value distribution theory is defined as the sum of two pieces: a proximity term measuring how close f gets to a on circles of radius r, and a counting term that counts occurrences of a inside the disk of radius r, weighted by multiplicity.
Русский
Характеристическая функция теории распределения значений задаётся как сумма двух слагаемых: проксимисная функция, измеряющая близость f к a по окружностям радиуса r, и счётная функция, подсчитывающая число вхождений a внутри диска радиуса r, взвешенное по кратности.
LaTeX
$$$\text{characteristic}(f,a) = \text{proximity}(f,a) + \text{logCounting}(f,a)$$$
Lean4
/-- The Characteristic Function of Value Distribution Theory
If `f : ℂ → E` is meromorphic and `a : WithTop E` is any value, the characteristic function of `f`
is defined as the sum of two terms: the proximity function, which quantifies how close `f` gets to
`a` on the circle `∣z∣ = r`, and the counting function, which counts the number times that `f`
attains the value `a` inside the disk `∣z∣ ≤ r`, weighted by multiplicity.
-/
noncomputable def characteristic : ℝ → ℝ :=
proximity f a + logCounting f a
