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 Section VI.2 of [Lang, Introduction to Complex Hyperbolic Spaces][MR886677] or Section 1.1 of [Noguchi-Winkelmann, Nevanlinna Theory in Several Complex Variables and Diophantine Approximation][MR3156076] 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.

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 Proximity Function

theorem ValueDistribution.proximity_congr_codiscreteWithin {E : Type u_1} [NormedAddCommGroup E] {f g : ℂ → E} {a : WithTop E} {r : ℝ} (hfg : f =ᶠ[Filter.codiscreteWithin (Metric.sphere 0 |r|)] g) (hr : r ≠ 0) : proximity f a r = proximity g a r

If two functions differ only on a discrete set, then their proximity functions agree, except perhaps at radius 0.

theorem ValueDistribution.proximity_congr_codiscrete {E : Type u_1} [NormedAddCommGroup E] {f g : ℂ → E} {a : WithTop E} {r : ℝ} (hfg : f =ᶠ[Filter.codiscrete ℂ] g) (hr : r ≠ 0) : proximity f a r = proximity g a r

If two functions differ only on a discrete set, then their proximity functions agree, except perhaps at radius 0.

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⁻¹.

theorem ValueDistribution.proximity_sub_proximity_inv_eq_circleAverage {f : ℂ → ℂ} (h₁f : Meromorphic f) : proximity f ⊤ - proximity f⁻¹ ⊤ = Real.circleAverage (fun (x : ℂ) => Real.log ‖f x‖) 0

For complex-valued f, the difference between proximity f ⊤ and proximity f⁻¹ ⊤ is the circle average of log ‖f ·‖.

theorem ValueDistribution.proximity_even {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {a : WithTop E} : Function.Even (proximity f a)

The proximity function is even.

theorem ValueDistribution.proximity_nonneg {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {a : WithTop E} : 0 ≤ proximity f a

The proximity function is non-negative.

@[simp]

theorem ValueDistribution.proximity_const {E : Type u_1} [NormedAddCommGroup E] {c : E} {r : ℝ} : proximity (fun (x : ℂ) => c) ⊤ r = ‖c‖.posLog

Behaviour under Arithmetic Operations

theorem ValueDistribution.proximity_sum_top_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {α : Type u_2} (s : Finset α) (f : α → ℂ → E) (hf : ∀ (a : α), Meromorphic (f a)) : proximity (∑ a ∈ s, f a) ⊤ ≤ ∑ a ∈ s, proximity (f a) ⊤ + fun (x : ℝ) => Real.log ↑s.card

The proximity function of a sum of functions at ⊤ is less than or equal to the sum of the proximity functions of the summand, plus log of the number of summands.

theorem ValueDistribution.proximity_add_top_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f₁ f₂ : ℂ → E} (h₁f₁ : Meromorphic f₁) (h₁f₂ : Meromorphic f₂) : proximity (f₁ + f₂) ⊤ ≤ proximity f₁ ⊤ + proximity f₂ ⊤ + fun (x : ℝ) => Real.log 2

The proximity function of f + g at ⊤ is less than or equal to the sum of the proximity functions of f and g, plus log 2 (where 2 is the number of summands).

theorem ValueDistribution.proximity_mul_top_le {f₁ f₂ : ℂ → ℂ} (h₁f₁ : Meromorphic f₁) (h₁f₂ : Meromorphic f₂) : proximity (f₁ * f₂) ⊤ ≤ proximity f₁ ⊤ + proximity f₂ ⊤

The proximity function f * g at ⊤ is less than or equal to the sum of the proximity functions of f and g, respectively.

@[deprecated ValueDistribution.proximity_mul_top_le (since := "2025-12-11")]

theorem ValueDistribution.proximity_top_mul_le {f₁ f₂ : ℂ → ℂ} (h₁f₁ : Meromorphic f₁) (h₁f₂ : Meromorphic f₂) : proximity (f₁ * f₂) ⊤ ≤ proximity f₁ ⊤ + proximity f₂ ⊤

Alias of ValueDistribution.proximity_mul_top_le.

---

The proximity function f * g at ⊤ is less than or equal to the sum of the proximity functions of f and g, respectively.

theorem ValueDistribution.proximity_mul_zero_le {f₁ f₂ : ℂ → ℂ} (h₁f₁ : Meromorphic f₁) (h₁f₂ : Meromorphic f₂) : proximity (f₁ * f₂) 0 ≤ proximity f₁ 0 + proximity f₂ 0

The proximity function f * g at 0 is less than or equal to the sum of the proximity functions of f and g, respectively.

@[deprecated ValueDistribution.proximity_mul_zero_le (since := "2025-12-11")]

theorem ValueDistribution.proximity_zero_mul_le {f₁ f₂ : ℂ → ℂ} (h₁f₁ : Meromorphic f₁) (h₁f₂ : Meromorphic f₂) : proximity (f₁ * f₂) 0 ≤ proximity f₁ 0 + proximity f₂ 0

Alias of ValueDistribution.proximity_mul_zero_le.

---

The proximity function f * g at 0 is less than or equal to the sum of the proximity functions of f and g, respectively.

@[simp]

theorem ValueDistribution.proximity_pow_top {f : ℂ → ℂ} {n : ℕ} : proximity (f ^ n) ⊤ = n • proximity f ⊤

For natural numbers n, the proximity function of f ^ n at ⊤ equals n times the proximity function of f at ⊤.

@[simp]

theorem ValueDistribution.proximity_pow_zero {f : ℂ → ℂ} {n : ℕ} : proximity (f ^ n) 0 = n • proximity f 0

For natural numbers n, the proximity function of f ^ n at 0 equals n times the proximity function of f at 0.