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