Cartan's Formula

This file will, in the future, establish Cartan's classic formula, describing the characteristic function characteristic f ⊤ r as a sum of two circle averages,

• circleAverage (logCounting f · r) 0 1 and
• circleAverage (fun a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖) 0 1.

As a corollary, Cartan's formula implies the (surprising, non-trival) fact that the characteristic function is monotone.

At present, this file establishes circle integrability of the function a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖ and computes values of the circle integral.

References

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

Terms in Cartan's formula

theorem ValueDistribution.circleIntegrable_log_meromorphicTrailingCoeffAt {f : ℂ → ℂ} : CircleIntegrable (fun (a : ℂ) => Real.log ‖meromorphicTrailingCoeffAt (fun (x : ℂ) => f x - a) 0‖) 0 1

Circle integrability of the term fun a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖ that appears in Cartan's formula.

theorem ValueDistribution.circleAverage_log_norm_meromorphicTrailingCoeffAt_of_meromorphicOrderAt_pos {f : ℂ → ℂ} (h : 0 < meromorphicOrderAt f 0) : Real.circleAverage (fun (a : ℂ) => Real.log ‖meromorphicTrailingCoeffAt (fun (x : ℂ) => f x - a) 0‖) 0 1 = 0

Circle average of the function fun a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖ that appears in Cartan's formula, in case where f has a zero at the origin.

theorem ValueDistribution.circleAverage_log_norm_meromorphicTrailingCoeffAt_of_meromorphicOrderAt_eq_zero {f : ℂ → ℂ} (h : meromorphicOrderAt f 0 = 0) : Real.circleAverage (fun (a : ℂ) => Real.log ‖meromorphicTrailingCoeffAt (fun (x : ℂ) => f x - a) 0‖) 0 1 = ‖meromorphicTrailingCoeffAt f 0‖.posLog

Circle average of the function fun a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖ that appears in Cartan's formula, in case where f has order zero at the origin.

theorem ValueDistribution.circleAverage_log_norm_meromorphicTrailingCoeffAt_of_meromorphicOrderAt_lt_zero {f : ℂ → ℂ} (h : meromorphicOrderAt f 0 < 0) : Real.circleAverage (fun (a : ℂ) => Real.log ‖meromorphicTrailingCoeffAt (fun (x : ℂ) => f x - a) 0‖) 0 1 = Real.log ‖meromorphicTrailingCoeffAt f 0‖

Circle average of the function fun a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖ that appears in Cartan's formula, in case where f has a pole at the origin.

theorem ValueDistribution.circleIntegrable_logCounting {f : ℂ → ℂ} {R : ℝ} (h : Meromorphic f) : CircleIntegrable (fun (x : ℂ) => logCounting f (↑x) R) 0 1

Circle integrability of the term logCounting f · R that appears in Cartan's formula.

Cartan's formula

theorem ValueDistribution.characteristic_top_eq_circleAverage_add_circleAverage {f : ℂ → ℂ} {R : ℝ} (h : Meromorphic f) (hR : R ≠ 0) : characteristic f ⊤ R = Real.circleAverage (fun (x : ℂ) => logCounting f (↑x) R) 0 1 + Real.circleAverage (fun (a : ℂ) => Real.log ‖meromorphicTrailingCoeffAt (fun (x : ℂ) => f x - a) 0‖) 0 1

Cartan's formula with the additive constant written explicitly as a circle average of the logarithm of the first nonzero Laurent coefficient of f - a at the origin.

See circleIntegrable_logCounting and circleIntegrable_log_trailingCoeff_of_meromorphic for the facts that the summands are actually circle integrable.

theorem ValueDistribution.characteristic_top_eq_circleAverage_of_meromorphicOrderAt_pos {f : ℂ → ℂ} {R : ℝ} (h₁f : Meromorphic f) (h₂f : 0 < meromorphicOrderAt f 0) (hR : R ≠ 0) : characteristic f ⊤ R = Real.circleAverage (fun (x : ℂ) => logCounting f (↑x) R) 0 1

Cartan's formula in case where 0 < meromorphicOrderAt f 0.

theorem ValueDistribution.characteristic_top_eq_circleAverage_add_const {f : ℂ → ℂ} (h : Meromorphic f) : ∃ (const : ℝ), ∀ (R : ℝ), R ≠ 0 → characteristic f ⊤ R = Real.circleAverage (fun (x : ℂ) => logCounting f (↑x) R) 0 1 + const

Qualitative version of Cartan's formula: Away from the point 0, the difference between characteristic f ⊤ and circleAverage (logCounting f · ·) 0 1 is constant. This qualitative version of Cartan's formula exists because the specific value of the constant does not matter in practise.

Application: Monotonicity of the Characteristic Function

theorem ValueDistribution.characteristic_monotoneOn {f : ℂ → ℂ} (h : Meromorphic f) : MonotoneOn (characteristic f ⊤) (Set.Ioi 0)

The characteristic function is monotone on (0, ∞). This result is surprisingly non-trivial, given that the proximity function is not monotone in general.