The Proximity Function of Value Distribution Theory

This file defines the "proximity function" attached to a meromorphic function defined on the complex plane. Also known as the Nevanlinna Proximity Function, this is one of the three main functions used in Value Distribution Theory.

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. The definition ensures that large values correspond to good approximation.

See SectionVI.2 of Lang, Introduction to Complex Hyperbolic Spaces or Section1.1 of Noguchi-Winkelmann, Nevanlinna Theory in Several Complex Variables and Diophantine Approximation for a detailed discussion.

noncomputable def ValueDistribution.proximity {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) (a : 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.

Equations

• ValueDistribution.proximity f a = if h : a = ⊤ then Real.circleAverage (fun (x : ℂ) => ‖f x‖.posLog) 0 else Real.circleAverage (fun (x : ℂ) => ‖f x - a.untop₀‖⁻¹.posLog) 0

theorem ValueDistribution.proximity_coe {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {a₀ : E} : proximity f ↑a₀ = Real.circleAverage (fun (x : ℂ) => ‖f x - a₀‖⁻¹.posLog) 0

Expand the definition of proximity f a₀ in case where a₀ is finite.

theorem ValueDistribution.proximity_zero {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} : proximity f 0 = Real.circleAverage (fun (x : ℂ) => ‖f x‖⁻¹.posLog) 0

Expand the definition of proximity f a₀ in case where a₀ is zero.

theorem ValueDistribution.proximity_zero_of_complexValued {f : ℂ → ℂ} : proximity f 0 = Real.circleAverage (fun (x : ℂ) => ‖f⁻¹ x‖.posLog) 0

For complex-valued functions, expand the definition of proximity f a₀ in case where a₀ is zero. This is a simple variant of proximity_zero defined above.

theorem ValueDistribution.proximity_top {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} : proximity f ⊤ = Real.circleAverage (fun (x : ℂ) => ‖f x‖.posLog) 0

Expand the definition of proximity f a in case where a₀ = ⊤.

Elementary Properties of the Counting Function

theorem ValueDistribution.proximity_coe_eq_proximity_sub_const_zero {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {a₀ : E} : proximity f ↑a₀ = proximity (f - fun (x : ℂ) => a₀) 0

For finite values a₀, the proximity function proximity f a₀ equals the proximity function for the value zero of the shifted function f - a₀.

theorem ValueDistribution.proximity_inv {f : ℂ → ℂ} : proximity f⁻¹ ⊤ = proximity f 0

For complex-valued f, establish a simple relation between the proximity functions of f and of f⁻¹.