Canonical Decomposition

If a function f is meromorphic on a compact set U, then it has only finitely many zeros and poles on the disk, and the theorem MeromorphicOn.extract_zeros_poles can be used to re-write f as (∏ᶠ u, (· - u) ^ divisor f U u) • g, where g is analytic without zeros on U. In case where U is a disk, one consider a similar decomposition, called Finite Canonical Decomposition or Finite Blaschke Product that replaces the factors (· - u) by canonical factors that take only values of norm one on the boundary of the disk. This file introduces the canonical factors and provides API for the canonical decomposition.

See Page 160f of Lang, Introduction to Complex Hyperbolic Spaces for a detailed discussion.

TODO: Formulate a refined version of the canonical decomposition that takes zeros on poles on the boundary of the ball into account.

Canonical Factors

Given R : ℝ and w : ℂ, the canonical factor canonical R w : ℂ → ℂ is meromorphic function in normal form that has a single pole at w, no zeros, and takes values of norm one on the circle of radius R.

noncomputable def Complex.canonicalFactor (R : ℝ) (w : ℂ) : ℂ → ℂ

Given R : ℝ and w : ℂ, the canonical factor is the function fun z ↦ (R ^ 2 - (conj w) * z) / (R * (z - w)). In applications, one will typically consider a setting where w ∈ ball 0 R.

Equations

• Complex.canonicalFactor R w z = (↑R ^ 2 - (starRingEnd ℂ) w * z) / (↑R * (z - w))

theorem Complex.canonicalFactor_def (R : ℝ) (w : ℂ) : canonicalFactor R w = fun (z : ℂ) => (↑R ^ 2 - (starRingEnd ℂ) w * z) / (↑R * (z - w))

theorem Complex.canonicalFactor_apply (R : ℝ) (w z : ℂ) : canonicalFactor R w z = (↑R ^ 2 - (starRingEnd ℂ) w * z) / (↑R * (z - w))

@[simp]

theorem Complex.canonicalFactor_apply_self (R : ℝ) (w : ℂ) : canonicalFactor R w w = 0

Regularity properties

theorem Complex.meromorphic_canonicalFactor (R : ℝ) (w : ℂ) : Meromorphic (canonicalFactor R w)

Canonical factors are meromorphic.

theorem Complex.analyticOnNhd_canonicalFactor (R : ℝ) (w : ℂ) : AnalyticOnNhd ℂ (canonicalFactor R w) {w}ᶜ

The canonical factor CanonicalFactor R w is analytic on the complement of w.

theorem Complex.meromorphicOrderAt_canonicalFactor {R : ℝ} {w : ℂ} (h : w ∈ Metric.ball 0 R) : meromorphicOrderAt (canonicalFactor R w) w = -1

The canonical factor CanonicalFactor R w has a simple pole at z = w.

theorem Complex.meromorphicNFOn_canonicalFactor {R : ℝ} {w : ℂ} (h : w ∈ Metric.ball 0 R) : MeromorphicNFOn (canonicalFactor R w) Set.univ

Canonical factors are meromorphic in normal form.

Values of Canonical Factors

theorem Complex.canonicalFactor_ne_zero {R : ℝ} {w z : ℂ} (hw : w ∈ Metric.ball 0 R) (h₁z : z ∈ Metric.closedBall 0 R) (h₂z : z ≠ w) : canonicalFactor R w z ≠ 0

The canonical factor CanonicalFactor R w has no zeros inside the ball of radius R.

theorem Complex.canonicalFactor_eq_zero_iff {R : ℝ} {w z : ℂ} (hw : w ∈ Metric.ball 0 R) (hz : z ∈ Metric.ball 0 R) : canonicalFactor R w z = 0 ↔ z = w

The function CanonicalFactor R w vanishes only at w.

theorem Complex.norm_canonicalFactor_eval_circle_eq_one {R : ℝ} {w z : ℂ} (hw : w ∈ Metric.ball 0 R) (hz : z ∈ Metric.sphere 0 R) : ‖canonicalFactor R w z‖ = 1

The canonical factor CanonicalFactor R w takes values of norm one on sphere 0 R.

Orders and Divisors

theorem Complex.meromorphicOrderAt_canonicalFactor_ne_top {z : ℂ} {R : ℝ} (w : ℂ) (hR : 0 < R) : meromorphicOrderAt (canonicalFactor R w) z ≠ ⊤

Canonical factors are nowhere locally constant zero.

theorem Complex.divisor_canonicalFactor {R : ℝ} {w : ℂ} (hw : w ∈ Metric.ball 0 R) : MeromorphicOn.divisor (canonicalFactor R w) (Metric.ball 0 R) = -Function.locallyFinsuppWithin.restrict (Function.locallyFinsuppWithin.single w 1) ⋯

The divisor of CanonicalFactor R w is -w. In other words, the divisor function takes the value -1 at w and is zero elsewhere.

Canonical Decomposition

The canonical decomposition theorem shows that a meromorphic function f on a disk is equal, up to modification over a discrete set, to a product of canonical factors and a meromorphic function g without zeros or poles in the interior of the disk.

To simplify notation and avoid repetition, we introduce a structure, CanonicalDecomp, that bundles the conclusions of the decomposition theorem.

structure Complex.CanonicalDecomp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f g : ℂ → E) (R : ℝ) : Prop

Given functions f, g and a real number R, the following convenience structure packs the information relevant in the canonical decomposition. The condition "g is without zeros or poles" is formulated by saying that g is meromorphic in normal form and g ≠ 0.

• meromorphicOn : MeromorphicOn f (Metric.closedBall 0 R)

  A proof that f is meromorphic on closedBall 0 R.

• meromorphicNFOn : MeromorphicNFOn g (Metric.closedBall 0 R)

  A proof that g is meromorphic in normal form on closedBall 0 R.

• ne_zero (u : ℂ) : u ∈ Metric.ball 0 R → g u ≠ 0

  A proof that g does not vanish in the interior of the ball.

• eventuallyEq : f =ᶠ[Filter.codiscreteWithin (Metric.closedBall 0 R)] (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(MeromorphicOn.divisor f (Metric.ball 0 R)) u)) • g

  A proof that f is equal, up to modification over a discrete set, to a product of g and canonical factors prescribed by the divisor of f.

theorem MeromorphicOn.exists_canonicalDecomp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {R : ℝ} {f : ℂ → E} (h₁f : MeromorphicOn f (Metric.closedBall 0 R)) (h₂f : ∀ (u : ↑(Metric.closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤) : ∃ (g : ℂ → E), Complex.CanonicalDecomp f g R

Canonical decomposition: A meromorphic function f on a disk is equal, up to modification over a discrete set, to a product of canonical factors and a meromorphic function g without zeros or poles in the interior of the disk.