Representation

Abstract

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

The CMV blocks use the positive Szego normalization at each real Schur parameter.

$\forall (k:\mathbb{N}),{\rho }_k=D5.S3.Weil.Szego.CanonicalTransfer.szegoRho({\alpha }_k:\mathbb{C})=\sqrt{1-|{\alpha }_k{|}^2}$

Definition 1.1 (R).

$$\forall (x:\mathbb{N}),Rx=\mathrm{if}x=0\mathrm{then}\left(\begin{array}{cc}\mathrm{alpha}0& D5.S3.Weil.Szego.CanonicalTransfer.szegoRhoComplex.ofReal\left((\mathrm{alpha}0)\right)\\ D5.S3.Weil.Szego.CanonicalTransfer.szegoRhoComplex.ofReal\left((\mathrm{alpha}0)\right)\cdot \mathrm{alpha}1& -\mathrm{alpha}0\cdot \mathrm{alpha}1\end{array}\right)\mathrm{else}\left(\begin{array}{cc}-\mathrm{alpha}(2\cdot x-1)\cdot \mathrm{alpha}(2\cdot x)& -\mathrm{alpha}(2\cdot x-1)\cdot D5.S3.Weil.Szego.CanonicalTransfer.szegoRhoComplex.ofReal\left((\mathrm{alpha}(2\cdot x))\right)\\ D5.S3.Weil.Szego.CanonicalTransfer.szegoRhoComplex.ofReal\left((\mathrm{alpha}(2\cdot x))\right)\cdot \mathrm{alpha}(2\cdot x+1)& -\mathrm{alpha}(2\cdot x)\cdot \mathrm{alpha}(2\cdot x+1)\end{array}\right)$$

Formalization. D5/S3/Quantum/Walks/CMV/Representation.R (✓ 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 2, arXiv PDF p. 2: “From the Verblunsky parameters, the corresponding QW on ℤ≥ is determined by” the displayed block matrix. The diagonal site blocks of the transposed CMV walk, with the boundary block R₀ stated separately, Section 2.

Definition 1.2 (P).

$$\forall (x:\mathbb{N}),Px=\left(\begin{array}{cc}D5.S3.Weil.Szego.CanonicalTransfer.szegoRhoComplex.ofReal\left((\mathrm{alpha}(2\cdot x))\right)\cdot D5.S3.Weil.Szego.CanonicalTransfer.szegoRhoComplex.ofReal\left((\mathrm{alpha}(2\cdot x+1))\right)& -\mathrm{alpha}(2\cdot x)\cdot D5.S3.Weil.Szego.CanonicalTransfer.szegoRhoComplex.ofReal\left((\mathrm{alpha}(2\cdot x+1))\right)\\ 0& 0\end{array}\right)$$

Formalization. D5/S3/Quantum/Walks/CMV/Representation.P (✓ 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 2, arXiv PDF p. 2: “From the Verblunsky parameters, the corresponding QW on ℤ≥ is determined by” the displayed block matrix. The block carrying amplitudes from site x to site x+1, Section 2.

Definition 1.3 (Q).

$$\forall (x:\mathbb{N}),Qx=\left(\begin{array}{cc}0& 0\\ D5.S3.Weil.Szego.CanonicalTransfer.szegoRhoComplex.ofReal\left((\mathrm{alpha}(2\cdot x-1))\right)\cdot \mathrm{alpha}(2\cdot x)& D5.S3.Weil.Szego.CanonicalTransfer.szegoRhoComplex.ofReal\left((\mathrm{alpha}(2\cdot x-1))\right)\cdot D5.S3.Weil.Szego.CanonicalTransfer.szegoRhoComplex.ofReal\left((\mathrm{alpha}(2\cdot x))\right)\end{array}\right)$$

Formalization. D5/S3/Quantum/Walks/CMV/Representation.Q (✓ 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 2, arXiv PDF p. 2: “From the Verblunsky parameters, the corresponding QW on ℤ≥ is determined by” the displayed block matrix. The block carrying amplitudes from site x to site x−1, Section 2.

Definition 1.4 (step).

$$\forall (v:\mathbb{N}\to \mathbb{R})(j:\mathbb{N}),\mathrm{step}vj=\mathrm{let}x:=Nat.divj2;\mathrm{let}i:=Fin.ofNat2j;(\sum (c:Fin2),Rxic\cdot v(2\cdot x+Fin.valc))+(\mathrm{if}x=0\mathrm{then}0\mathrm{else}\sum (c:Fin2),P(x-1)ic\cdot v(2\cdot (x-1)+Fin.valc))+(\sum (c:Fin2),Q(x+1)ic\cdot v(2\cdot (x+1)+Fin.valc))$$

Formalization. D5/S3/Quantum/Walks/CMV/Representation.step (✓ 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 2, arXiv PDF p. 2: “The evolution is defined by the equation Ψₜ₊₁ = U⁽ˢ⁾Ψₜ, where Ψₜ = [Ψₜ(0), Ψₜ(1), Ψₜ(2), …]ᵀ.” The coordinates 2x and 2x+1 are respectively the left and right components. The boundary omits the term from site −1. Division by 2 is natural-number division rounded down.

Definition 1.5 (psi).

$$\begin{array}{r}\mathrm{psi}0=Pi.single01\\ \forall (t:\mathbb{N}),\mathrm{psi}(t+1)=\mathrm{step}(\mathrm{psi}t)\end{array}$$

Formalization. D5/S3/Quantum/Walks/CMV/Representation.psi (✓ 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 2, arXiv PDF p. 2: “The evolution is defined by the equation Ψₜ₊₁ = U⁽ˢ⁾Ψₜ, where Ψₜ = [Ψₜ(0), Ψₜ(1), Ψₜ(2), …]ᵀ.” The initial flattened amplitude is Pi.single 0 1, representing Ψ₀ = [1, 0]ᵀδ₀.

Definition 1.6 (mu).

$$\forall (tx:\mathbb{N}),\mathrm{mu}tx=(\mathrm{psi}t(2\cdot x){)}^2+(\mathrm{psi}t(2\cdot x+1){)}^2$$

Formalization. D5/S3/Quantum/Walks/CMV/Representation.mu (✓ 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 2, arXiv PDF p. 2: “Then the probability of location x at time t is given by μₜ(x)=‖Ψₜ(x)‖²=|Ψₜᴸ(x)|²+|Ψₜᴿ(x)|².” The two real components are psi t (2x) and psi t (2x+1).

Theorem 1.7 (mu outside).

$$\forall (tx:\mathbb{N}),t<x\to \mathrm{mu}tx=0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/Representation.mu_outside (✓ 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 natural time t and site x with t strictly less than x, the walk probability mu t x is zero.

Definition 1.8 (SpectralBridge).

$$\forall (chi:\mathbb{N}\to LaurentPolynomial\mathbb{R}),\mathrm{SpectralBridge}chi⟺(chi0=LaurentPolynomial.T0)\wedge (\forall (ij:\mathbb{N}),\mathrm{sigma}(chii)(chij)=\mathrm{if}i=j\mathrm{then}1\mathrm{else}0)\wedge (\forall (Y:\mathbb{N}),Submodule.span\mathbb{R}(Set.imagechi\{j:\mathbb{N}\mid j<2\cdot Y+2\})=VY)\wedge (\forall (q:LaurentPolynomial\mathbb{R})(j:\mathbb{N}),\mathrm{sigma}(chij)(LaurentPolynomial.T(-1)\cdot q)=\mathrm{step}(\mathrm{fun}(k:\mathbb{N})\mapsto \mathrm{sigma}(chik)q)j)$$

Formalization. D5/S3/Quantum/Walks/CMV/Representation.SpectralBridge (✓ 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.

A Laurent polynomial sequence satisfies SpectralBridge when its first term is the constant monomial, it is sigma orthonormal, its first twice Y plus two terms span V Y for every natural Y, and pairing with multiplication by the monomial at negative one acts by step on its coefficient sequence.

Definition 1.9 (cumulative).

$$\forall (nY:\mathbb{N}),\mathrm{cumulative}nY=\sum y\in Finset.range(Y+1),\mathrm{mu}ny$$

Formalization. D5/S3/Quantum/Walks/CMV/Representation.cumulative (✓ 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 natural time n and site Y, cumulative n Y is the sum of the walk probabilities over sites zero through Y inclusive.

Theorem 1.10 (amplitude spectral).

$$\forall \{chi:\mathbb{N}\to LaurentPolynomial\mathbb{R}\},\mathrm{SpectralBridge}chi\to \forall (tj:\mathbb{N}),\mathrm{psi}tj=(\mathrm{sigma}(chij))(LaurentPolynomial.T(-Nat.cast\left(t\right)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/Representation.amplitude_spectral (✓ 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 Laurent polynomial sequence satisfies SpectralBridge, then for every natural time t and coordinate j, psi t j equals the sigma pairing of its jth term with the Laurent monomial at negative t.

Theorem 1.11 (cumulative projection).

$$\forall \{chi:\mathbb{N}\to LaurentPolynomial\mathbb{R}\},\mathrm{SpectralBridge}chi\to \forall (nY:\mathbb{N}),\exists (h:LaurentPolynomial\mathbb{R}),\mathrm{IsProjection}\mathrm{sigma}(VY)(LaurentPolynomial.T(-Nat.cast\left(n\right)))h\wedge (\mathrm{sigma}h)h=\mathrm{cumulative}nY$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/Representation.cumulative_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 Laurent polynomial sequence satisfies SpectralBridge, then for natural n and Y there is a sigma projection of the monomial at negative n onto V Y whose sigma pairing with itself equals cumulative n Y.

Definition 1.12 (PairRelations).

$$\forall (chixi:\mathbb{N}\to LaurentPolynomial\mathbb{R}),\mathrm{PairRelations}chixi⟺(chi0=xi0)\wedge (\forall (x:\mathbb{N}),chi(2\cdot x+1)=\mathrm{alpha}(2\cdot x+1)\cdot xi(2\cdot x+1)+D5.S3.Weil.Szego.CanonicalTransfer.szegoRho(Complex.ofReal(\mathrm{alpha}(2\cdot x+1)))\cdot xi(2\cdot x+2))\wedge (\forall (x:\mathbb{N}),1\le x\to chi(2\cdot x)=D5.S3.Weil.Szego.CanonicalTransfer.szegoRho(Complex.ofReal(\mathrm{alpha}(2\cdot x-1)))\cdot xi(2\cdot x-1)-\mathrm{alpha}(2\cdot x-1)\cdot xi(2\cdot x))\wedge (\forall (x:\mathbb{N}),LaurentPolynomial.T1\cdot xi(2\cdot x)=\mathrm{alpha}(2\cdot x)\cdot chi(2\cdot x)+D5.S3.Weil.Szego.CanonicalTransfer.szegoRho(Complex.ofReal(\mathrm{alpha}(2\cdot x)))\cdot chi(2\cdot x+1))\wedge (\forall (x:\mathbb{N}),LaurentPolynomial.T1\cdot xi(2\cdot x+1)=D5.S3.Weil.Szego.CanonicalTransfer.szegoRho(Complex.ofReal(\mathrm{alpha}(2\cdot x)))\cdot chi(2\cdot x)-\mathrm{alpha}(2\cdot x)\cdot chi(2\cdot x+1))$$

Formalization. D5/S3/Quantum/Walks/CMV/Representation.PairRelations (✓ 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.

Two Laurent polynomial sequences satisfy PairRelations when their first terms agree, their odd and positive even terms satisfy the displayed relations using alpha and szegoRho at odd indices, and multiplication by the monomial at exponent one satisfies the two displayed relations at even parameter indices.

Theorem 1.13 (one step of pair relations).

$$\forall \{chixi:\mathbb{N}\to LaurentPolynomial\mathbb{R}\},\mathrm{PairRelations}chixi\to \forall (q:LaurentPolynomial\mathbb{R})(j:\mathbb{N}),(\mathrm{sigma}(chij))(LaurentPolynomial.T(-1)\cdot q)=\mathrm{step}(\mathrm{fun}(k:\mathbb{N})\mapsto (\mathrm{sigma}(chik))q)j$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/Representation.one_step_of_pair_relations (✓ 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 chi and xi satisfy PairRelations, then for every real Laurent polynomial q and natural j, pairing chi j with q multiplied by the monomial at negative one equals step applied to the sequence of sigma pairings with q at coordinate j.

Definition 1.14 (alternate).

$$\forall (j:\mathbb{N}),\mathrm{alternate}j=\mathrm{if}j\mathrm{mod}2=0\mathrm{then}LaurentPolynomial.T(-Nat.cast\left((Nat.divj2)\right))\cdot \mathrm{normalizedPhi}j\mathrm{else}LaurentPolynomial.T(-Nat.cast\left((Nat.divj2)\right)-1)\cdot \mathrm{normalizedPhiStar}j$$

Formalization. D5/S3/Quantum/Walks/CMV/Representation.alternate (✓ 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 natural index j, alternate j shifts normalizedPhi j by negative half of j when j is even, and shifts normalizedPhiStar j by negative half of j minus one when j is odd; division by two is natural-number division rounded down. For natural arguments, mod denotes Nat.mod, the remainder of natural-number division.

Theorem 1.15 (pair relations of parameters).

$$(\forall (n:\mathbb{N}),\mathrm{alpha}n=\mathrm{verblunsky}n)\to \mathrm{PairRelations}\mathrm{chi}\mathrm{alternate}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Walks/CMV/Representation.pair_relations_of_parameters (✓ 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 alpha n equals verblunsky n for every natural n, the sequences chi and alternate satisfy PairRelations.

References

• Truth anchor: D5/S3/Quantum/Walks/CMV/Representation.P
• Truth anchor: D5/S3/Quantum/Walks/CMV/Representation.PairRelations
• Truth anchor: D5/S3/Quantum/Walks/CMV/Representation.Q
• Truth anchor: D5/S3/Quantum/Walks/CMV/Representation.R
• Truth anchor: D5/S3/Quantum/Walks/CMV/Representation.SpectralBridge
• Truth anchor: D5/S3/Quantum/Walks/CMV/Representation.alternate
• Truth anchor: D5/S3/Quantum/Walks/CMV/Representation.amplitude_spectral
• Truth anchor: D5/S3/Quantum/Walks/CMV/Representation.cumulative
• Truth anchor: D5/S3/Quantum/Walks/CMV/Representation.cumulative_projection
• Truth anchor: D5/S3/Quantum/Walks/CMV/Representation.mu
• Truth anchor: D5/S3/Quantum/Walks/CMV/Representation.mu_outside
• Truth anchor: D5/S3/Quantum/Walks/CMV/Representation.one_step_of_pair_relations
• Truth anchor: D5/S3/Quantum/Walks/CMV/Representation.pair_relations_of_parameters
• Truth anchor: D5/S3/Quantum/Walks/CMV/Representation.psi
• Truth anchor: D5/S3/Quantum/Walks/CMV/Representation.step
• Dependency: D5/S3/Quantum/Walks/CMV/Geronimus