Integral Presentation of the Proximity Function

If f : ℂ → ℂ is meromorphic, this file establishes a presentation of the proximity function proximity f ⊤ as iterated circle averages. This statement can be used to compare the proximity- and logarithmic counting functions, and is one of the key ingredients in the proof of Cartan's classic formula for the characteristic function.

See Section VI.2 of [Lang, Introduction to Complex Hyperbolic Spaces][MR886677] for a detailed discussion.

Integrability of the Cartan Kernel

The proof of the integral presentation of the proximity function relies on an extended computation, applying Fubini's theorem to the Cartan kernel of integration. This section defines the kernel and establishes its integrability, as a function of two variables.

noncomputable def ValueDistribution.Cartan.cartanKernel (f : ℂ → ℂ) (R α β : ℝ) : ℝ

Given f : ℂ → ℂ and R : ℝ, define the Cartan kernel of integration as the function α β ↦ log ‖f (circleMap 0 R β) - circleMap 0 1 α‖.

Equations

• ValueDistribution.Cartan.cartanKernel f R α β = Real.log ‖f (circleMap 0 R β) - circleMap 0 1 α‖

theorem ValueDistribution.Cartan.integrableOn_cartanKernel_left (f : ℂ → ℂ) (R β : ℝ) : MeasureTheory.IntegrableOn (fun (x : ℝ) => cartanKernel f R x β) (Set.Ioc 0 (2 * Real.pi)) MeasureTheory.volume

For every function f : ℂ → ℂ, the Cartan kernel of integration cartanKernel f R α β is integrable as a function in α.

theorem ValueDistribution.Cartan.measurable_cartanKernel {f : ℂ → ℂ} {R : ℝ} (hf : Measurable f) : Measurable fun (p : ℝ × ℝ) => cartanKernel f R p.1 p.2

If f : ℂ → ℂ is measurable, then the Cartan kernel of integration is measurable as a function in the two variables α and β.

theorem ValueDistribution.Cartan.integrable_integral_norm_cartanKernel {f : ℂ → ℂ} {R : ℝ} (h : Meromorphic f) : MeasureTheory.Integrable (fun (x : ℝ) => ∫ (α : ℝ) in Set.Ioc 0 (2 * Real.pi), ‖cartanKernel f R α x‖) (MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi)))

theorem ValueDistribution.Cartan.integrableOn_cartanKernel {f : ℂ → ℂ} {R : ℝ} (h : Meromorphic f) : MeasureTheory.IntegrableOn (fun (p : ℝ × ℝ) => cartanKernel f R p.1 p.2) (Set.uIoc 0 (2 * Real.pi) ×ˢ Set.uIoc 0 (2 * Real.pi)) MeasureTheory.volume

If f : ℂ → ℂ is meromorphic, then the Cartan kernel of integration is integrable as a function in the two variables α and β.

theorem ValueDistribution.Cartan.integrableOn_intervalIntegral_cartanKernel_left {f : ℂ → ℂ} {R : ℝ} (h : Meromorphic f) : MeasureTheory.IntegrableOn (fun (x : ℝ) => ∫ (α : ℝ) in 0..2 * Real.pi, cartanKernel f R α x) (Set.Ioc 0 (2 * Real.pi)) MeasureTheory.volume

Corollary of integrableOn_cartanKernel: If f : ℂ → ℂ is meromorphic, then the function β ↦ ∫ α in 0..2 * π, Cartan.cartanKernel f R α β is integrable.

theorem ValueDistribution.Cartan.integrableOn_intervalIntegral_cartanKernel_right {f : ℂ → ℂ} {R : ℝ} (h : Meromorphic f) : MeasureTheory.IntegrableOn (fun (x : ℝ) => ∫ (β : ℝ) in 0..2 * Real.pi, cartanKernel f R x β) (Set.Ioc 0 (2 * Real.pi)) MeasureTheory.volume

Corollary of integrableOn_cartanKernel: If f : ℂ → ℂ is meromorphic, then the function α ↦ ∫ β in 0..2 * π, Cartan.cartanKernel f R α β is integrable.

theorem ValueDistribution.circleAverage_circleAverage_eq_proximity_top {f : ℂ → ℂ} (h : Meromorphic f) : (fun (R : ℝ) => Real.circleAverage (fun (a : ℂ) => Real.circleAverage (fun (x : ℂ) => Real.log ‖f x - a‖) 0 R) 0 1) = proximity f ⊤

Presentation of the proximity function as iterated circle averages.

theorem ValueDistribution.circleIntegrable_circleAverage_log_norm_sub {f : ℂ → ℂ} {R : ℝ} (h : Meromorphic f) : CircleIntegrable (fun (a : ℂ) => Real.circleAverage (fun (x : ℂ) => Real.log ‖f x - a‖) 0 R) 0 1

Complementary statement to proximity_top_eq_circleAverage_circleAverage, providing circle integrability of the integrand.