Cartan's Formula

This file establishes Cartan's classic formula, ValueDistribution.characteristic_top_eq_circleAverage_add_circleAverage, 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 (surprisingly non-trivial) fact that the characteristic function is monotone; this is stated in ValueDistribution.characteristic_monotoneOn.

This file also establishes circle integrability of the function a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖ and computes values of the circle average.

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 the 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 the 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 the 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_meromorphicTrailingCoeffAt 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 the 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 fun R ↦ circleAverage (logCounting f · R) 0 1 is constant. This qualitative version of Cartan's formula exists because the specific value of the constant does not matter in practice.

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.