Finite Disk Blaschke Multipliers

Abstract

Zeros in the disk and a unit phase construct the actual bounded isometric Blaschke multiplier on the full Hardy coefficient space.

H2 is the full complex lp2 coefficient space constructed in HardyCoefficientRealization. Operator multiplication means composition. Complex inner products are conjugate-linear in their first argument.

Definition 1.1 (The unilateral coefficient shift).

$$Q:H^2\to H^2,\forall f\in H^2,n\in \mathbb{N},\mathrm{coeff}(\mathrm{apply}(Q,f),0)=0,\mathrm{coeff}(\mathrm{apply}(Q,f),n+1)=\mathrm{coeff}(f,n)$$

Formalization. D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.shift (✓ std3).

Source. Repository-derived.

Commentary.

Q is a complex-linear isometry. The zero and successor coefficient equations are also exposed as shift_zero and shift_succ.

Theorem 1.2 (The shift multiplies evaluation by z).

$$\forall f\in H^2,z\in \mathbb{C},|z|<1\Rightarrow \mathrm{evaluate}(\mathrm{apply}(Q,f),z)=z\mathrm{evaluate}(f,z)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.shift_evaluate (✓ std3). ∎

Source. Repository-derived.

Commentary.

This is equality of the actual convergent coefficient-series evaluations.

Definition 1.3 (The Neumann denominator is a unit).

$$\forall a\in \mathbb{C},|a|<1\Rightarrow \mathrm{denominatorUnit}(a)=I-\overline{a}Q$$

Formalization. D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.denominatorUnit (✓ std3).

Source. Repository-derived.

Commentary.

The value is I-conjugate(a)Q in the bounded-operator algebra. Mathlib’s Units.oneSub constructs its inverse from the norm-convergent geometric series. No inverse is assumed for an arbitrary bounded operator.

Definition 1.4 (The concrete single-factor multiplier).

$$\forall a\in \mathbb{C},|a|<1\Rightarrow \mathrm{factor}(a)=(Q-aI)(I-\overline{a}Q{)}^{-1}$$

Formalization. D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.factor (✓ std3).

Source. Repository-derived.

Commentary.

The inverse is the already constructed unit inverse.

Theorem 1.5 (Single-factor analytic multiplication).

$$\forall a\in \mathbb{C},|a|<1\Rightarrow \forall f\in H^2,z\in \mathbb{C},|z|<1\Rightarrow \mathrm{evaluate}(\mathrm{apply}(\mathrm{factor}(a),f),z)=\frac{z-a}{1-\overline{a}z}\mathrm{evaluate}(f,z)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.factor_evaluate (✓ std3). ∎

Source. Repository-derived.

Commentary.

The operator evaluates as multiplication by (z-a)/(1-conjugate(a)z).

Theorem 1.6 (Every disk factor is isometric).

$$\forall a\in \mathbb{C},|a|<1\Rightarrow \mathrm{Isometry}(\mathrm{factor}(a))$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.factor_isometry (✓ std3). ∎

Source. Repository-derived.

Commentary.

The proof expands ||Qy-ay|| squared and ||y-conjugate(a)Qy|| squared, then applies the constructed inverse denominator.

Definition 1.7 (Only zeros and phase are data).

$$a:\mathrm{Fin}(m)\to \mathrm{UnitDisc},c\in \mathrm{Circle}$$

Formalization. D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.FiniteBlaschkeData (✓ std3).

Source. Repository-derived.

Commentary.

The zeros may repeat. The fields contain no isometry, model dimension, kernel normalization, orthonormality or invariance assumption.

Definition 1.8 (The finite Blaschke product).

$$\forall m\in \mathbb{N},B\in \mathrm{FiniteBlaschkeData}(m),\mathrm{value}(B,z)=\mathrm{phase}(B)\prod _{j\in \mathrm{Fin}(m)}\frac{z-\mathrm{zero}(B,j)}{1-\overline{\mathrm{zero}(B,j)}z}$$

Formalization. D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.value (✓ std3).

Source. Repository-derived.

Commentary.

Lean evaluates the product using List.ofFn in canonical Fin order.

Definition 1.9 (The bounded finite-product operator).

$$\forall m\in \mathbb{N},B\in \mathrm{FiniteBlaschkeData}(m),\mathrm{mul}(B)=\mathrm{phase}(B)\prod _{j\in \mathrm{Fin}(m)}\mathrm{factor}(\mathrm{zero}(B,j))$$

Formalization. D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.mul (✓ std3).

Source. Repository-derived.

Commentary.

This is the ordered operator product from List.ofFn, scaled by the unit phase.

Theorem 1.10 (The actual multiplication law).

$$\forall m\in \mathbb{N},B\in \mathrm{FiniteBlaschkeData}(m),\forall f\in H^2,z\in \mathbb{C},|z|<1\Rightarrow \mathrm{evaluate}(\mathrm{apply}(\mathrm{mul}(B),f),z)=\mathrm{value}(B,z)\mathrm{evaluate}(f,z)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.mul_eval (✓ std3). ∎

Source. Repository-derived.

Commentary.

The constructed continuous linear map is actual analytic multiplication by B.

Theorem 1.11 (The finite multiplier is isometric).

$$\forall m\in \mathbb{N},B\in \mathrm{FiniteBlaschkeData}(m),\mathrm{Isometry}(\mathrm{mul}(B))$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.mul_isometry (✓ std3). ∎

Source. Repository-derived.

Commentary.

Composition of the proved factor isometries and a unit scalar preserves the full H2 norm.

Theorem 1.12 (Positive degree maps the disk strictly into itself).

$$\forall m\in \mathbb{N},B\in \mathrm{FiniteBlaschkeData}(m),0<m\Rightarrow \forall z\in \mathbb{C},|z|<1\Rightarrow |\mathrm{value}(B,z)|<1$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.maps_unitDisc (✓ std3). ∎

Source. Repository-derived.

Commentary.

The strict factor bound follows from the positive defect (1-|a| squared)(1-|z| squared). Positive degree makes the product nonempty.

Definition 1.13 (The zero polynomial product).

$$\forall m\in \mathbb{N},B\in \mathrm{FiniteBlaschkeData}(m),\mathrm{numerator}(B)=\prod _{j\in \mathrm{Fin}(m)}(T-C(\mathrm{zero}(B,j)))$$

Formalization. D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.numerator (✓ std3).

Source. Repository-derived.

Commentary.

T is the polynomial indeterminate and C embeds a complex constant.

Definition 1.14 (The denominator polynomial).

$$\forall m\in \mathbb{N},B\in \mathrm{FiniteBlaschkeData}(m),\mathrm{denominator}(B)=\prod _{j\in \mathrm{Fin}(m)}(1-C(\overline{\mathrm{zero}(B,j)})T)$$

Formalization. D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.denominator (✓ std3).

Source. Repository-derived.

Commentary.

This polynomial is distinct from the coefficient-shift operator Q above.

Definition 1.15 (The actual phase polynomial).

$$\forall m\in \mathbb{N},B\in \mathrm{FiniteBlaschkeData}(m),\forall alpha\in \mathrm{Circle},\mathrm{fibrePolynomial}(B,alpha)=C(\mathrm{phase}(B))\mathrm{numerator}(B)-C(alpha)\mathrm{denominator}(B)$$

Formalization. D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.fibrePolynomial (✓ std3).

Source. Repository-derived.

Commentary.

Every alpha on the circle is permitted.

Definition 1.16 (The boundary Poisson weight).

$$\forall m\in \mathbb{N},B\in \mathrm{FiniteBlaschkeData}(m),\forall zeta\in \mathrm{Circle},\mathrm{poissonWeight}(B,zeta)=\sum _{j\in \mathrm{Fin}(m)}\frac{1-|\mathrm{zero}(B,j){|}^2}{|zeta-\mathrm{zero}(B,j){|}^2}$$

Formalization. D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.poissonWeight (✓ std3).

Source. Repository-derived.

Commentary.

The weight is real and uses the actual disk zeros, including multiplicities.

Theorem 1.17 (No factor pole on the closed disk).

$$\forall a\in \mathrm{UnitDisc},z\in \mathbb{C},|z|\le 1\Rightarrow 1-\overline{a}z\ne 0$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.factor_denominator_ne_zero_closed (✓ std3). ∎

Source. Repository-derived.

Commentary.

The strict zero-parameter norm and closed-disk bound imply nonvanishing.

Theorem 1.18 (The full denominator has no closed-disk zero).

$$\forall m\in \mathbb{N},B\in \mathrm{FiniteBlaschkeData}(m),\forall z\in \mathbb{C},|z|\le 1\Rightarrow \mathrm{eval}(\mathrm{denominator}(B),z)\ne 0$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.denominator_ne_zero_closed (✓ std3). ∎

Source. Repository-derived.

Commentary.

This supplies the analytic extension domain used by the actual model space.

Theorem 1.19 (The finite product is the polynomial quotient).

$$\forall m\in \mathbb{N},B\in \mathrm{FiniteBlaschkeData}(m),\forall z\in \mathbb{C},\mathrm{value}(B,z)=\frac{\mathrm{phase}(B)\mathrm{eval}(\mathrm{numerator}(B),z)}{\mathrm{eval}(\mathrm{denominator}(B),z)}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.value_eq_polynomial_div (✓ std3). ∎

Source. Repository-derived.

Commentary.

The equality holds for every complex z under Lean’s total division convention.

Theorem 1.20 (Origin normalization forces a zero parameter).

$$\forall m\in \mathbb{N},B\in \mathrm{FiniteBlaschkeData}(m),\mathrm{value}(B,0)=0\Rightarrow \exists j\in \mathrm{Fin}(m),\mathrm{zero}(B,j)=0$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.zero_parameter (✓ std3). ∎

Source. Repository-derived.

Commentary.

The zero parameter is derived from B(0)=0, not added as an assumption.

Theorem 1.21 (The numerator has degree m).

$$\forall m\in \mathbb{N},B\in \mathrm{FiniteBlaschkeData}(m),\mathrm{natDegree}(\mathrm{numerator}(B))=m$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.numerator_natDegree (✓ std3). ∎

Source. Repository-derived.

Commentary.

Pinned Mathlib’s monic product theorem supplies the exact degree.

Theorem 1.22 (The normalized denominator has smaller degree).

$$\forall m\in \mathbb{N},B\in \mathrm{FiniteBlaschkeData}(m),\mathrm{value}(B,0)=0\Rightarrow \mathrm{natDegree}(\mathrm{denominator}(B))<m$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.denominator_natDegree_lt (✓ std3). ∎

Source. Repository-derived.

Commentary.

The derived zero parameter removes one linear denominator factor.

Theorem 1.23 (Every phase polynomial has degree m).

$$\forall m\in \mathbb{N},B\in \mathrm{FiniteBlaschkeData}(m),\forall alpha\in \mathrm{Circle},\mathrm{value}(B,0)=0\Rightarrow \mathrm{natDegree}(\mathrm{fibrePolynomial}(B,alpha))=m$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.fibrePolynomial_natDegree (✓ std3). ∎

Source. Repository-derived.

Commentary.

The unit numerator coefficient cannot cancel against a denominator of smaller degree.

Theorem 1.24 (Every phase-polynomial root is an actual circle preimage).

$$\forall m\in \mathbb{N},B\in \mathrm{FiniteBlaschkeData}(m),\forall alpha\in \mathrm{Circle},\forall z\in \mathbb{C},0<m\wedge \mathrm{value}(B,0)=0\wedge \mathrm{eval}(\mathrm{fibrePolynomial}(B,alpha),z)=0\Rightarrow |z|=1\wedge \mathrm{value}(B,z)=alpha$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.fibre_root (✓ std3). ∎

Source. Repository-derived.

Commentary.

Poles are excluded first. Strict factor modulus estimates exclude exterior roots; the proved disk mapping excludes interior roots.

Theorem 1.25 (The Poisson weight is positive).

$$\forall m\in \mathbb{N},B\in \mathrm{FiniteBlaschkeData}(m),\forall zeta\in \mathrm{Circle},0<m\Rightarrow 0<\mathrm{poissonWeight}(B,zeta)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.poissonWeight_pos (✓ std3). ∎

Source. Repository-derived.

Commentary.

Positive degree supplies a nonempty sum of strictly positive terms.

Theorem 1.26 (The exact analytic boundary derivative).

$$\forall m\in \mathbb{N},B\in \mathrm{FiniteBlaschkeData}(m),\forall zeta\in \mathrm{Circle},\mathrm{HasDerivAt}(\mathrm{value}(B),\frac{\mathrm{value}(B,zeta)}{zeta}\mathrm{poissonWeight}(B,zeta),zeta)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.value_hasDerivAt_circle (✓ std3). ∎

Source. Repository-derived.

Commentary.

This is a complex derivative in a neighborhood of the circle point. The real Poisson weight is coerced to the complex field.

Theorem 1.27 (The phase-polynomial derivative at a fibre point).

$$\forall m\in \mathbb{N},B\in \mathrm{FiniteBlaschkeData}(m),\forall alpha\in \mathrm{Circle},\forall zeta\in \mathrm{Circle},\mathrm{value}(B,zeta)=alpha\Rightarrow \mathrm{eval}(\mathrm{derivative}(\mathrm{fibrePolynomial}(B,alpha)),zeta)=\mathrm{eval}(\mathrm{denominator}(B),zeta)\frac{alpha}{zeta}\mathrm{poissonWeight}(B,zeta)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.fibre_derivative (✓ std3). ∎

Source. Repository-derived.

Commentary.

This is R’(zeta)=Q(zeta)B’(zeta), with the exact positive Poisson expression substituted.

Theorem 1.28 (Every phase has exactly m distinct simple circle preimages).

$$\forall m\in \mathbb{N},B\in \mathrm{FiniteBlaschkeData}(m),\forall alpha\in \mathrm{Circle},0<m\wedge \mathrm{value}(B,0)=0\Rightarrow \exists zeta:\mathrm{Fin}(m)\to \mathrm{Circle},\mathrm{Injective}(zeta)\wedge (\forall z\in \mathbb{C},(\mathrm{value}(B,z)=alpha\wedge |z|=1)⟺(\exists j\in \mathrm{Fin}(m),z=\mathrm{apply}(zeta,j)))\wedge (\forall j\in \mathrm{Fin}(m),\mathrm{eval}(\mathrm{derivative}(\mathrm{fibrePolynomial}(B,alpha)),\mathrm{apply}(zeta,j))\ne 0)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.phase_fibre (✓ std3). ∎

Source. Repository-derived.

Commentary.

The finite family exhausts the fibre, is injective, and every root is simple. Complex polynomial splitting and separability supply the exact cardinality.

The source normalization B(0)=0 remains explicit. ClarkKernelRealization uses these actual all-phase fibres and positive derivatives for its analytic boundary kernels and normalization.

References

• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.FiniteBlaschkeData
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.denominator
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.denominatorUnit
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.denominator_natDegree_lt
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.denominator_ne_zero_closed
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.factor
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.factor_denominator_ne_zero_closed
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.factor_evaluate
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.factor_isometry
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.fibrePolynomial
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.fibrePolynomial_natDegree
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.fibre_derivative
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.fibre_root
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.maps_unitDisc
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.mul
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.mul_eval
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.mul_isometry
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.numerator
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.numerator_natDegree
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.phase_fibre
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.poissonWeight
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.poissonWeight_pos
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.shift
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.shift_evaluate
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.value
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.value_eq_polynomial_div
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.value_hasDerivAt_circle
• Truth anchor: D5/S3/Analytic/Hardy/FiniteBlaschkeMultiplier.zero_parameter
• Dependency: D5/S3/Analytic/Hardy/HardyCoefficientRealization