SzegoRecurrence

Abstract

Finite Riesz moments, orthogonal Laurent polynomials and scale-four projection identities.

Definition 1.1 (residue).

$$\forall (da:\mathbb{Z}),\mathrm{residue}da=Submodule.span\mathbb{R}(Set.image(LaurentPolynomial.T)(\{e:\mathbb{Z}\mid e\mathrm{mod}d=a\}))$$

Formalization. D5/S3/Quantum/Walks/CMV/SzegoRecurrence.residue (✓ std3).

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For integers d and a, residue d a is the real span of Laurent monomials whose integer exponent has remainder a modulo d. For integer arguments, mod denotes the Euclidean remainder: for nonzero d it lies between 0 inclusive and abs(d) exclusive, and e mod 0 equals e.

Definition 1.2 (W).

$$\forall (x:\mathbb{N}),Wx=Submodule.span\mathbb{R}(Set.image(LaurentPolynomial.T)(\{e:\mathbb{Z}\mid -(2\cdot Nat.cast\left(x\right))\le e\wedge e\le 2\cdot Nat.cast\left(x\right)\}))$$

Formalization. D5/S3/Quantum/Walks/CMV/SzegoRecurrence.W (✓ std3).

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural x, W x is the real span of Laurent monomials with integer exponents from minus twice x through twice x, including both endpoints.

Definition 1.3 (E).

$$\forall (x:\mathbb{N}),Ex=Submodule.span\mathbb{R}(Set.image(LaurentPolynomial.T)(\{e:\mathbb{Z}\mid -(2\cdot Nat.cast\left(x\right))\le e\wedge e\le 2\cdot Nat.cast\left(x\right)\wedge e\mathrm{mod}2=0\}))$$

Formalization. D5/S3/Quantum/Walks/CMV/SzegoRecurrence.E (✓ std3).

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural x, E x is the real span of Laurent monomials with even integer exponents from minus twice x through twice x, including both endpoints. For integer arguments, mod denotes the Euclidean remainder: for nonzero d it lies between 0 inclusive and abs(d) exclusive, and e mod 0 equals e.

Definition 1.4 (IsProjection).

$$\forall (B:LaurentPolynomial\mathbb{R}{\to }_l[\mathbb{R}]LaurentPolynomial\mathbb{R}{\to }_l[\mathbb{R}]\mathbb{R})(V:Submodule\mathbb{R}(LaurentPolynomial\mathbb{R}))(fh:LaurentPolynomial\mathbb{R}),\mathrm{IsProjection}BVfh⟺(h\in V)\wedge (\forall (q:LaurentPolynomial\mathbb{R}),q\in V\to Bq(f-h)=0)$$

Formalization. D5/S3/Quantum/Walks/CMV/SzegoRecurrence.IsProjection (✓ std3).

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For a real bilinear form B, a Laurent subspace V and Laurent polynomials f and h, IsProjection holds exactly when h belongs to V and every q in V has zero B pairing with f minus h.

Theorem 1.5 (T mem spanOn).

$$\forall \{S:Set\mathbb{Z}\}\{e:\mathbb{Z}\},e\in S\to (LaurentPolynomial.Te)\in Submodule.span\mathbb{R}(Set.image(LaurentPolynomial.T)(S))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.T_mem_spanOn (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

If an integer exponent e belongs to a set S, its Laurent monomial belongs to the real span of the monomials with exponents in S.

Theorem 1.6 (spanOn mono).

$$\forall \{SSprime:Set\mathbb{Z}\},S\subseteq Sprime\to Submodule.span\mathbb{R}(Set.image(LaurentPolynomial.T)(S))\le Submodule.span\mathbb{R}(Set.image(LaurentPolynomial.T)(Sprime))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.spanOn_mono (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

If a set of integer exponents S is contained in another set, the real span of its Laurent monomials is contained in the real span of the monomials from the larger set.

Theorem 1.7 (form zero on span).

$$\forall (B:LaurentPolynomial\mathbb{R}{\to }_l[\mathbb{R}]LaurentPolynomial\mathbb{R}{\to }_l[\mathbb{R}]\mathbb{R})(S:Set\mathbb{Z})(r:LaurentPolynomial\mathbb{R}),(\forall (e:\mathbb{Z}),e\in S\to (B(LaurentPolynomial.Te))r=0)\to \forall (q:LaurentPolynomial\mathbb{R}),q\in Submodule.span\mathbb{R}(Set.image(LaurentPolynomial.T)(S))\to (Bq)r=0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.form_zero_on_span (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For a real bilinear form B and a Laurent polynomial r, if every monomial with exponent in S has zero B pairing with r, every Laurent polynomial in their real span also has zero pairing with r.

Theorem 1.8 (residue class orthogonal).

$$\forall (B:LaurentPolynomial\mathbb{R}{\to }_l[\mathbb{R}]LaurentPolynomial\mathbb{R}{\to }_l[\mathbb{R}]\mathbb{R})(dab:\mathbb{Z}),a\ne b\to (\forall (ij:\mathbb{Z}),i\mathrm{mod}d\ne j\mathrm{mod}d\to (B(LaurentPolynomial.Ti))(LaurentPolynomial.Tj)=0)\to \forall (p:LaurentPolynomial\mathbb{R}),p\in \mathrm{residue}da\to \forall (q:LaurentPolynomial\mathbb{R}),q\in \mathrm{residue}db\to (Bp)q=0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.residue_class_orthogonal (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

If a real bilinear form B pairs monomials with different integer remainders modulo d to zero, then it pairs every polynomial in residue d a with every polynomial in residue d b to zero whenever a and b are distinct integers. For integer arguments, mod denotes the Euclidean remainder: for nonzero d it lies between 0 inclusive and abs(d) exclusive, and e mod 0 equals e.

Theorem 1.9 (E le W).

$$\forall (x:\mathbb{N}),Ex\le Wx$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.E_le_W (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural x, the even-exponent window E x is contained in the full Laurent window W x.

Theorem 1.10 (E le even).

$$\forall (x:\mathbb{N}),Ex\le \mathrm{residue}20$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.E_le_even (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural x, E x is contained in the Laurent subspace residue 2 0.

Theorem 1.11 (projection unique).

$$\forall (B:LaurentPolynomial\mathbb{R}{\to }_l[\mathbb{R}]LaurentPolynomial\mathbb{R}{\to }_l[\mathbb{R}]\mathbb{R})(V:Submodule\mathbb{R}(LaurentPolynomial\mathbb{R})),(\forall (p:LaurentPolynomial\mathbb{R}),p\ne 0\to 0<(Bp)p)\to \forall \{fhk:LaurentPolynomial\mathbb{R}\},\mathrm{IsProjection}BVfh\to \mathrm{IsProjection}BVfk\to h=k$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.projection_unique (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

If a real bilinear form B is strictly positive on every nonzero Laurent polynomial paired with itself, any two B projections of the same Laurent polynomial onto the same subspace are equal.

Theorem 1.12 (finite projection exists).

$$\forall (B:LaurentPolynomial\mathbb{R}{\to }_l[\mathbb{R}]LaurentPolynomial\mathbb{R}{\to }_l[\mathbb{R}]\mathbb{R})(V:Submodule\mathbb{R}(LaurentPolynomial\mathbb{R}))[FiniteDimensional\mathbb{R}CoeSort.coe\left(V\right)],(\forall (p:LaurentPolynomial\mathbb{R}),p\ne 0\to 0<(Bp)p)\to \forall (f:LaurentPolynomial\mathbb{R}),\exists (h:LaurentPolynomial\mathbb{R}),\mathrm{IsProjection}BVfh$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.finite_projection_exists (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For a real bilinear form B that is strictly positive on every nonzero Laurent polynomial paired with itself, each Laurent polynomial has a B projection onto every finite-dimensional real Laurent subspace.

Theorem 1.13 (finite orthonormal projection).

$$\forall (B:LaurentPolynomial\mathbb{R}{\to }_l[\mathbb{R}]LaurentPolynomial\mathbb{R}{\to }_l[\mathbb{R}]\mathbb{R})(v:\mathbb{N}\to LaurentPolynomial\mathbb{R}),(\forall (ij:\mathbb{N}),(B(vi))(vj)=\mathrm{if}i=j\mathrm{then}1\mathrm{else}0)\to \forall (N:\mathbb{N})(f:LaurentPolynomial\mathbb{R}),\mathrm{have}V:=Submodule.span\mathbb{R}(Set.image(v)(\{j:\mathbb{N}\mid j<N\}));\mathrm{have}h:=\sum j\in Finset.rangeN,(B(vj))f\cdot vj;\mathrm{IsProjection}BVfh\wedge (Bh)h=\sum j\in Finset.rangeN,((B(vj))f{)}^2$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.finite_orthonormal_projection (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

If a sequence of real Laurent polynomials is orthonormal for a real bilinear form B, the sum of the first N polynomials weighted by their B pairings with f is a B projection of f onto their span. Its B pairing with itself is the sum of the squares of those N pairings.

Definition 1.14 (V).

$$\forall (Y:\mathbb{N}),VY=Submodule.span\mathbb{R}(Set.image(LaurentPolynomial.T)(\{e:\mathbb{Z}\mid -Nat.cast\left(Y\right)\le e\wedge e\le Nat.cast\left(Y\right)+1\}))$$

Formalization. D5/S3/Quantum/Walks/CMV/SzegoRecurrence.V (✓ std3).

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural Y, V Y is the real span of Laurent monomials with integer exponents from minus Y through Y plus one, including both endpoints.

Definition 1.15 (W finite).

$$\forall (x:\mathbb{N}),FiniteDimensional\mathbb{R}CoeSort.coe\left((Wx)\right)$$

Formalization. D5/S3/Quantum/Walks/CMV/SzegoRecurrence.W_finite (✓ std3).

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural x, the real Laurent subspace W x is finite-dimensional.

Definition 1.16 (E finite).

$$\forall (x:\mathbb{N}),FiniteDimensional\mathbb{R}CoeSort.coe\left((Ex)\right)$$

Formalization. D5/S3/Quantum/Walks/CMV/SzegoRecurrence.E_finite (✓ std3).

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural x, the real Laurent subspace E x is finite-dimensional.

Definition 1.17 (innerCore).

$$\begin{array}{r}\mathrm{innerCore}:InnerProductSpace.Core\mathbb{R}(LaurentPolynomial\mathbb{R})\\ \forall (xy:LaurentPolynomial\mathbb{R}),innerCore.innerxy=\mathrm{sigma}xy\\ \forall (xy:LaurentPolynomial\mathbb{R}),\mathrm{sigma}xy=\mathrm{sigma}yx\\ \forall (x:LaurentPolynomial\mathbb{R}),0\le \mathrm{sigma}xx\\ \forall (xyz:LaurentPolynomial\mathbb{R}),\mathrm{sigma}(x+y)z=\mathrm{sigma}xz+\mathrm{sigma}yz\\ \forall (xy:LaurentPolynomial\mathbb{R})(r:\mathbb{R}),\mathrm{sigma}(r\cdot x)y=r\cdot \mathrm{sigma}xy\\ \forall (x:LaurentPolynomial\mathbb{R}),\mathrm{sigma}xx=0\to x=0\end{array}$$

Formalization. D5/S3/Quantum/Walks/CMV/SzegoRecurrence.innerCore (✓ std3).

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

The form sigma supplies a real inner product core on Laurent polynomials, with symmetry, nonnegativity, linearity and definiteness.

Definition 1.18 (exponent).

$$\forall (j:\mathbb{N}),\mathrm{exponent}j=\mathrm{if}j\mathrm{mod}2=0\mathrm{then}-Nat.cast\left((Nat.divj2)\right)\mathrm{else}Nat.cast\left((Nat.divj2)\right)+1$$

Formalization. D5/S3/Quantum/Walks/CMV/SzegoRecurrence.exponent (✓ std3).

Citation. Ryota Hanaoka, Norio Konno (2021). Return probability and self-similarity of the Riesz walk. DOI: 10.26421/QIC21.5-6-5. URL: https://arxiv.org/abs/2010.04518v3.

Commentary.

Section 3, arXiv PDF p. 8: “Laurent polynomials {χⱼ}ⱼ₌₀∞ are obtained from the Gram-Schmidt orthonormalization of {1,z,z⁻¹,z²,z⁻²,…}.” The Laurent monomials are ordered 0,1,−1,2,−2,… . Division by 2 is natural-number division rounded down. For natural arguments, mod denotes Nat.mod, the remainder of natural-number division.

Definition 1.19 (monomials).

$$\forall (j:\mathbb{N}),\mathrm{monomials}j=LaurentPolynomial.T(\mathrm{exponent}j)$$

Formalization. D5/S3/Quantum/Walks/CMV/SzegoRecurrence.monomials (✓ std3).

Citation. Ryota Hanaoka, Norio Konno (2021). Return probability and self-similarity of the Riesz walk. DOI: 10.26421/QIC21.5-6-5. URL: https://arxiv.org/abs/2010.04518v3.

Commentary.

Section 3, arXiv PDF p. 8: “Laurent polynomials {χⱼ}ⱼ₌₀∞ are obtained from the Gram-Schmidt orthonormalization of {1,z,z⁻¹,z²,z⁻²,…}.” LaurentPolynomial.T and exponent give exactly this order.

Definition 1.20 (chi).

$$\mathrm{chi}=InnerProductSpace.gramSchmidtNormed\mathbb{R}\mathrm{monomials}$$

Formalization. D5/S3/Quantum/Walks/CMV/SzegoRecurrence.chi (✓ std3).

Citation. Ryota Hanaoka, Norio Konno (2021). Return probability and self-similarity of the Riesz walk. DOI: 10.26421/QIC21.5-6-5. URL: https://arxiv.org/abs/2010.04518v3.

Commentary.

Section 3, arXiv PDF p. 8: “Laurent polynomials {χⱼ}ⱼ₌₀∞ are obtained from the Gram-Schmidt orthonormalization of {1,z,z⁻¹,z²,z⁻²,…}.” The real moment inner product supplies the orthonormalization.

Theorem 1.21 (chi orthonormal).

$$\forall (ij:\mathbb{N}),(\mathrm{sigma}(\mathrm{chi}i))(\mathrm{chi}j)=\mathrm{if}i=j\mathrm{then}1\mathrm{else}0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.chi_orthonormal (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For all natural i and j, the sigma pairing of chi i and chi j is one when the indices coincide and zero otherwise.

Theorem 1.22 (chi window).

$$\forall (Y:\mathbb{N}),Submodule.span\mathbb{R}(Set.image(\mathrm{chi})(\{j:\mathbb{N}\mid j<2\cdot Y+2\}))=VY$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.chi_window (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural Y, the real span of chi j over indices less than twice Y plus two equals the Laurent window V Y.

Theorem 1.23 (chi zero).

$$\mathrm{chi}0=LaurentPolynomial.T0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.chi_zero (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

The first orthonormal Laurent polynomial chi 0 is the constant monomial with exponent zero.

Theorem 1.24 (sigma shift).

$$\forall (e:\mathbb{Z})(pq:LaurentPolynomial\mathbb{R}),(\mathrm{sigma}(LaurentPolynomial.Te\cdot p))(LaurentPolynomial.Te\cdot q)=(\mathrm{sigma}p)q$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.sigma_shift (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every integer e and real Laurent polynomials p and q, multiplying both polynomials by the Laurent monomial at e preserves their sigma pairing.

Theorem 1.25 (sigma shift adjoint).

$$\forall (e:\mathbb{Z})(pq:LaurentPolynomial\mathbb{R}),(\mathrm{sigma}p)(LaurentPolynomial.T(-e)\cdot q)=(\mathrm{sigma}(LaurentPolynomial.Te\cdot p))q$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.sigma_shift_adjoint (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every integer e and real Laurent polynomials p and q, the sigma pairing of p with q multiplied by the monomial at negative e equals the pairing of p multiplied by the monomial at e with q.

Definition 1.26 (coeffLM).

$$\forall (e:\mathbb{Z}),\mathrm{coeffLM}e=Finsupp.lapplye{\circ }_{l}LinearEquiv.toLinearMap\left((AddMonoidAlgebra.coeffLinearEquiv\mathbb{R})\right)$$

Formalization. D5/S3/Quantum/Walks/CMV/SzegoRecurrence.coeffLM (✓ std3).

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For an integer e, coeffLM e is the real linear map extracting the coefficient at exponent e from a real Laurent polynomial.

Theorem 1.27 (coeffLM T).

$$\forall (ej:\mathbb{Z}),(\mathrm{coeffLM}e)(LaurentPolynomial.Tj)=\mathrm{if}e=j\mathrm{then}1\mathrm{else}0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.coeffLM_T (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For integer exponents e and j, the coefficient at e of the Laurent monomial at j is one if the exponents coincide and zero otherwise.

Theorem 1.28 (mem spanOn iff).

$$\forall (S:Set\mathbb{Z})(p:LaurentPolynomial\mathbb{R}),p\in Submodule.span\mathbb{R}(Set.image(LaurentPolynomial.T)(S))⟺\forall (e:\mathbb{Z}),\neg e\in S\to (\mathrm{coeffLM}e)p=0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.mem_spanOn_iff (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For any set S of integer exponents, a real Laurent polynomial belongs to the real span of the monomials from S exactly when all its coefficients outside S vanish.

Definition 1.29 (polyWindow).

$$\forall (n:\mathbb{N}),\mathrm{polyWindow}n=Submodule.span\mathbb{R}(Set.image(LaurentPolynomial.T)(\{e:\mathbb{Z}\mid 0\le e\wedge e\le Nat.cast\left(n\right)\}))$$

Formalization. D5/S3/Quantum/Walks/CMV/SzegoRecurrence.polyWindow (✓ std3).

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n, polyWindow n is the real span of Laurent monomials with exponents from zero through n, including both endpoints.

Definition 1.30 (polyBelow).

$$\forall (n:\mathbb{N}),\mathrm{polyBelow}n=Submodule.span\mathbb{R}(Set.image(LaurentPolynomial.T)(\{e:\mathbb{Z}\mid 0\le e\wedge e<Nat.cast\left(n\right)\}))$$

Formalization. D5/S3/Quantum/Walks/CMV/SzegoRecurrence.polyBelow (✓ std3).

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n, polyBelow n is the real span of Laurent monomials with nonnegative exponents strictly less than n.

Definition 1.31 (phi).

$$\mathrm{phi}=InnerProductSpace.gramSchmidt\mathbb{R}\mathrm{fun}(n:\mathbb{N})\mapsto LaurentPolynomial.TNat.cast\left(n\right)$$

Formalization. D5/S3/Quantum/Walks/CMV/SzegoRecurrence.phi (✓ std3).

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

The sequence phi is obtained by applying real Gram-Schmidt orthogonalization, without normalization, to the Laurent monomials with natural exponents in increasing order.

Theorem 1.32 (phi mem window).

$$\forall (n:\mathbb{N}),(\mathrm{phi}n)\in \mathrm{polyWindow}n$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.phi_mem_window (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n, phi n belongs to polyWindow n.

Theorem 1.33 (coeff window zero).

$$\forall (n:\mathbb{N})\{p:LaurentPolynomial\mathbb{R}\},p\in \mathrm{polyWindow}n\to \forall (e:\mathbb{Z}),e<0\vee Nat.cast\left(n\right)<e\to (\mathrm{coeffLM}e)p=0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.coeff_window_zero (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

If a real Laurent polynomial belongs to polyWindow n, its coefficient at an integer exponent e is zero whenever e is negative or exceeds n.

Theorem 1.34 (phi monic).

$$\forall (n:\mathbb{N}),(\mathrm{coeffLM}Nat.cast\left(n\right))(\mathrm{phi}n)=1$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.phi_monic (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n, the coefficient of phi n at exponent n is one.

Theorem 1.35 (phi orthogonal).

$$\forall (n:\mathbb{N})(e:\mathbb{Z}),0\le e\wedge e<Nat.cast\left(n\right)\to (\mathrm{sigma}(LaurentPolynomial.Te))(\mathrm{phi}n)=0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.phi_orthogonal (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n and integer exponent e from zero inclusive to n exclusive, the sigma pairing of the monomial at e with phi n is zero.

Theorem 1.36 (phi orthogonal span).

$$\forall (n:\mathbb{N}),\forall (q:LaurentPolynomial\mathbb{R}),q\in \mathrm{polyBelow}n\to (\mathrm{sigma}q)(\mathrm{phi}n)=0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.phi_orthogonal_span (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n, every polynomial in polyBelow n has zero sigma pairing with phi n.

Definition 1.37 (phiStar).

$$\forall (n:\mathbb{N}),\mathrm{phiStar}n=LaurentPolynomial.TNat.cast\left(n\right)\cdot LaurentPolynomial.invert(\mathrm{phi}n)$$

Formalization. D5/S3/Quantum/Walks/CMV/SzegoRecurrence.phiStar (✓ std3).

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n, phiStar n is phi n with all exponents negated and then shifted by n.

Theorem 1.38 (phiStar norm).

$$\forall (n:\mathbb{N}),(\mathrm{sigma}(\mathrm{phiStar}n))(\mathrm{phiStar}n)=(\mathrm{sigma}(\mathrm{phi}n))(\mathrm{phi}n)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.phiStar_norm (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n, phiStar n and phi n have the same sigma pairing with themselves.

Theorem 1.39 (coeffLM shift).

$$\forall (ei:\mathbb{Z})(p:LaurentPolynomial\mathbb{R}),(\mathrm{coeffLM}e)(LaurentPolynomial.Ti\cdot p)=(\mathrm{coeffLM}(e-i))p$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.coeffLM_shift (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For integers e and i and a real Laurent polynomial p, the coefficient at e after multiplication by the monomial at i is the coefficient of p at e minus i.

Theorem 1.40 (coeffLM invert).

$$\forall (e:\mathbb{Z})(p:LaurentPolynomial\mathbb{R}),(\mathrm{coeffLM}e)(LaurentPolynomial.invertp)=(\mathrm{coeffLM}(-e))p$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.coeffLM_invert (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For an integer e and a real Laurent polynomial p, the coefficient at e after exponent inversion is the coefficient of p at negative e.

Theorem 1.41 (phiStar constant).

$$\forall (n:\mathbb{N}),(\mathrm{coeffLM}0)(\mathrm{phiStar}n)=1$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.phiStar_constant (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n, the constant coefficient of phiStar n is one.

Theorem 1.42 (phiStar coeff zero).

$$\forall (n:\mathbb{N})(e:\mathbb{Z}),e<0\vee Nat.cast\left(n\right)<e\to (\mathrm{coeffLM}e)(\mathrm{phiStar}n)=0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.phiStar_coeff_zero (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n, the coefficient of phiStar n at an integer exponent e is zero whenever e is negative or exceeds n.

Theorem 1.43 (phiStar orthogonal).

$$\forall (n:\mathbb{N})(e:\mathbb{Z}),1\le e\wedge e\le Nat.cast\left(n\right)\to (\mathrm{sigma}(LaurentPolynomial.Te))(\mathrm{phiStar}n)=0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.phiStar_orthogonal (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n and integer exponent e from one through n inclusive, the sigma pairing of the monomial at e with phiStar n is zero.

Theorem 1.44 (phiStar mem window).

$$\forall (n:\mathbb{N}),(\mathrm{phiStar}n)\in \mathrm{polyWindow}n$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.phiStar_mem_window (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n, phiStar n belongs to polyWindow n.

Definition 1.45 (verblunsky).

$$\forall (n:\mathbb{N}),\mathrm{verblunsky}n=-(\mathrm{coeffLM}0)(\mathrm{phi}(n+1))$$

Formalization. D5/S3/Quantum/Walks/CMV/SzegoRecurrence.verblunsky (✓ std3).

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n, verblunsky n is the negative of the constant coefficient of phi at index n plus one.

Theorem 1.46 (monic szego).

$$\forall (n:\mathbb{N}),\mathrm{phi}(n+1)=LaurentPolynomial.T1\cdot \mathrm{phi}n-\mathrm{verblunsky}n\cdot \mathrm{phiStar}n$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.monic_szego (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n, phi at index n plus one equals phi n multiplied by the monomial at exponent one, minus verblunsky n times phiStar n.

Definition 1.47 (normSquare).

$$\forall (n:\mathbb{N}),\mathrm{normSquare}n=(\mathrm{sigma}(\mathrm{phi}n))(\mathrm{phi}n)$$

Formalization. D5/S3/Quantum/Walks/CMV/SzegoRecurrence.normSquare (✓ std3).

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n, normSquare n is the sigma pairing of phi n with itself.

Theorem 1.48 (normSquare pos).

$$\forall (n:\mathbb{N}),0<\mathrm{normSquare}n$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.normSquare_pos (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n, normSquare n is strictly positive.

Theorem 1.49 (verblunsky sq lt one).

$$\forall (n:\mathbb{N}),(\mathrm{verblunsky}n{)}^2<1$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.verblunsky_sq_lt_one (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n, the square of the real Verblunsky coefficient verblunsky n is strictly less than one.

Definition 1.50 (gramNorm).

$$\forall (n:\mathbb{N}),\mathrm{gramNorm}n=\sqrt{(\mathrm{normSquare}n)}$$

Formalization. D5/S3/Quantum/Walks/CMV/SzegoRecurrence.gramNorm (✓ std3).

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n, gramNorm n is the real square root of normSquare n.

Definition 1.51 (normalizedPhi).

$$\forall (n:\mathbb{N}),\mathrm{normalizedPhi}n=(\mathrm{gramNorm}n{)}^{-1}\cdot \mathrm{phi}n$$

Formalization. D5/S3/Quantum/Walks/CMV/SzegoRecurrence.normalizedPhi (✓ std3).

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n, normalizedPhi n is phi n multiplied by the reciprocal of gramNorm n.

Definition 1.52 (normalizedPhiStar).

$$\forall (n:\mathbb{N}),\mathrm{normalizedPhiStar}n=(\mathrm{gramNorm}n{)}^{-1}\cdot \mathrm{phiStar}n$$

Formalization. D5/S3/Quantum/Walks/CMV/SzegoRecurrence.normalizedPhiStar (✓ std3).

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n, normalizedPhiStar n is phiStar n multiplied by the reciprocal of gramNorm n.

Theorem 1.53 (normalized szego).

$$\forall (n:\mathbb{N}),D5.S3.Weil.Szego.CanonicalTransfer.szegoRhoComplex.ofReal\left((\mathrm{verblunsky}n)\right)\cdot \mathrm{normalizedPhi}(n+1)=LaurentPolynomial.T1\cdot \mathrm{normalizedPhi}n-\mathrm{verblunsky}n\cdot \mathrm{normalizedPhiStar}n$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.normalized_szego (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n, szegoRho at verblunsky n times normalizedPhi at index n plus one equals normalizedPhi n multiplied by the monomial at exponent one, minus verblunsky n times normalizedPhiStar n.

Theorem 1.54 (monic star szego).

$$\forall (n:\mathbb{N}),\mathrm{phiStar}(n+1)=\mathrm{phiStar}n-\mathrm{verblunsky}n\cdot (LaurentPolynomial.T1\cdot \mathrm{phi}n)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.monic_star_szego (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n, phiStar at index n plus one equals phiStar n minus verblunsky n times phi n multiplied by the monomial at exponent one.

Theorem 1.55 (normalized star inverse).

$$\forall (n:\mathbb{N}),\mathrm{normalizedPhiStar}(n+1)=D5.S3.Weil.Szego.CanonicalTransfer.szegoRhoComplex.ofReal\left((\mathrm{verblunsky}n)\right)\cdot \mathrm{normalizedPhiStar}n-\mathrm{verblunsky}n\cdot \mathrm{normalizedPhi}(n+1)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.normalized_star_inverse (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural n, normalizedPhiStar at index n plus one equals szegoRho at verblunsky n times normalizedPhiStar n, minus verblunsky n times normalizedPhi at index n plus one.

Theorem 1.56 (chi even).

$$\forall (k:\mathbb{N}),\mathrm{chi}(2\cdot k)=LaurentPolynomial.T(-Nat.cast\left(k\right))\cdot \mathrm{normalizedPhiStar}(2\cdot k)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.chi_even (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural k, chi at index twice k equals normalizedPhiStar at that index multiplied by the Laurent monomial at negative k.

Theorem 1.57 (chi odd).

$$\forall (k:\mathbb{N}),\mathrm{chi}(2\cdot k+1)=LaurentPolynomial.T(-Nat.cast\left(k\right))\cdot \mathrm{normalizedPhi}(2\cdot k+1)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/SzegoRecurrence.chi_odd (✓ std3). ∎

Citation. Barry Simon (2005). Orthogonal Polynomials on the Unit Circle, Part 1: Classical Theory. DOI: 10.1090/coll054.1. URL: https://doi.org/10.1090/coll054.1.

Commentary.

For every natural k, chi at index twice k plus one equals normalizedPhi at that index multiplied by the Laurent monomial at negative k.

References

• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.E
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.E_finite
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.E_le_W
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.E_le_even
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.IsProjection
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.T_mem_spanOn
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.V
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.W
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.W_finite
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.chi
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.chi_even
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.chi_odd
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.chi_orthonormal
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.chi_window
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.chi_zero
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.coeffLM
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.coeffLM_T
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.coeffLM_invert
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.coeffLM_shift
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.coeff_window_zero
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.exponent
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.finite_orthonormal_projection
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.finite_projection_exists
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.form_zero_on_span
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.gramNorm
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.innerCore
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.mem_spanOn_iff
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.monic_star_szego
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.monic_szego
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.monomials
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.normSquare
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.normSquare_pos
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.normalizedPhi
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.normalizedPhiStar
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.normalized_star_inverse
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.normalized_szego
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.phi
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.phiStar
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.phiStar_coeff_zero
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.phiStar_constant
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.phiStar_mem_window
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.phiStar_norm
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.phiStar_orthogonal
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.phi_mem_window
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.phi_monic
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.phi_orthogonal
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.phi_orthogonal_span
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.polyBelow
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.polyWindow
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.projection_unique
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.residue
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.residue_class_orthogonal
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.sigma_shift
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.sigma_shift_adjoint
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.spanOn_mono
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.verblunsky
• Truth anchor: D5/S3/Quantum/Walks/CMV/SzegoRecurrence.verblunsky_sq_lt_one
• Dependency: D5/S3/Quantum/Walks/Riesz/Moments
• Dependency: D5/S3/Weil/Szego/CanonicalTransfer