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 Canonical Decomposition or Blaschke Product that replaces the factors (· - u) by canonical factors that take only values of norm one on the boundary of the circle. This file introduces the canonical factors.

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

TODO: Formulate the canonical decomposition.

Canonical Factors

Given R : ℝ and w : ℂ, the Blaschke factor Blaschke R w : ℂ → ℂ is meromorphic in normal form, 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.meromorphicOn_canonicalFactor (R : ℝ) (w : ℂ) : MeromorphicOn (canonicalFactor R w) Set.univ

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.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.