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.

TODO

• Establish Cartan's Formula in full
• Prove monotonicity of the characteristic function

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.