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.

This file also formulates an extended version of the canonical decomposition that takes zeros on poles on the boundary of the ball into account.

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

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.

theorem Complex.CanonicalDecomp.divisor_eq_divisor {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {R : ℝ} {f g : ℂ → E} {x : ℂ} (D : CanonicalDecomp f g R) (hR : 0 < R) : (MeromorphicOn.divisor g (Metric.closedBall 0 R)) x = (MeromorphicOn.divisor f (Metric.sphere 0 R)) x

Given a canonical decomposition CanonicalDecomp f g R, the function associated with the divisor of g equals the function associated with the divisor of f, seen as a meromorphic function on the sphere.

Extended Canonical Decomposition

The extended canonical decomposition theorem shows that a meromorphic function f on a closed disk is equal, up to modification over a discrete set, to a product of a non-vanishing analytic function, canonical factors and meromorphic functions of the form (x - const) ^ n where const is on the circumference of the disk.

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

structure Complex.ECanonicalDecomp {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 extended canonical decomposition.

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

  A proof that f is meromorphic on closedBall 0 R.

• analyticOnNhd : AnalyticOnNhd ℂ g (Metric.closedBall 0 R)

  A proof that g is analytic in a neighborhood of closedBall 0 R.

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

  A proof that g does not vanish on the closed ball.

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

  A proof that f is equal, up to modification over a discrete set, to a product of g, canonical factors prescribed by the divisor of f, and a factorized rational function with poles and zeros only on the boundary of the ball.

theorem MeromorphicOn.exists_ecanonicalDecomp {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 ≠ ⊤) : ∃ (h : ℂ → E), Complex.ECanonicalDecomp f h R

Extended canonical decomposition: A meromorphic function on a closed disk is equal, up to modification over a discrete set, to a product of a non-vanishing analytic function, canonical factors and meromorphic functions of the form (x - const) ^ n where const is on the circumference of the disk.