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 or Section 1.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 Proximity 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⁻¹.

theorem ValueDistribution.proximity_sub_proximity_inv_eq_circleAverage {f : ℂ → ℂ} (h₁f : MeromorphicOn 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 ·‖.

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 : α), MeromorphicOn (f a) Set.univ) : 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₁ : MeromorphicOn f₁ Set.univ) (h₁f₂ : MeromorphicOn f₂ Set.univ) : 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_top_mul_le {f₁ f₂ : ℂ → ℂ} (h₁f₁ : MeromorphicOn f₁ Set.univ) (h₁f₂ : MeromorphicOn f₂ Set.univ) : 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.

theorem ValueDistribution.proximity_zero_mul_le {f₁ f₂ : ℂ → ℂ} (h₁f₁ : MeromorphicOn f₁ Set.univ) (h₁f₂ : MeromorphicOn f₂ Set.univ) : 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.

@[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.