The exchange operator of two truncated oscillators

Two d-level oscillators (transmon-like ladders) coupled by an exchange interaction g E, where E = a† ⊗ a + a ⊗ a† and a is the truncated annihilation operator, a e_j = √j e_{j-1} (bd i j = √j if j = i + 1, else 0). Let Q = a + a† be the quadrature and λ a real eigenvalue of Q (the largest eigenvalue λ_d is the largest zero of the Hermite polynomial He_d, λ_d ~ 2 √d, DLMF 18.16.17 for the asymptotics) and κ_d = ‖E‖ the operator norm.

With ideal fast local control, the averaging framework of Wocjan–Rötteler–Janzing–Beth (Phys. Rev. A 65, 042309) gives for the controlled-Z time the sandwich π / (4 g κ_d) ≤ T_CZ ≤ π / (2 g λ_d²); the upper bound comes from a quadrature-code construction (E acts as (1/2) Q ⊗ Q on the quadrature code) and the lower bound from κ_d. None of this physics is formalized here; this file proves only the purely matrix-analytic sandwich between the two constants:

• QSL.Exchange.exchange_norm_ge: if x is a real unit eigenvector of Q with eigenvalue λ, then λ² / 2 ≤ ‖E‖ (Rayleigh quotient at x ⊗ x);
• QSL.Exchange.exchange_norm_le: ‖E‖ ≤ 2 (d - 1), via ‖a‖ ≤ √(d - 1);
• QSL.Exchange.ratio_sandwich: 1 ≤ 2 ‖E‖ / λ² ≤ 4 (d - 1) / λ².

Asymptotics (the ratio 2κ_d/λ_d² is the quotient of the CZ-time upper and lower bounds above, so → 1 says the two bounds agree to leading order):

• QSL.Exchange.lamMax: the largest eigenvalue λ_d of Q, the supremum of the Rayleigh quotient; quad_form_le_lamMax is the variational fact ⟪v, Q v⟫ ≤ λ_d ‖v‖² and exists_unit_eigenvector gives a unit eigenvector for λ_d (Mathlib's LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional);
• QSL.Exchange.lamMax_ge: the uniform test vector on the last m levels gives λ_d ≥ 2 (1 - 1/m) √(d - m) for 2 ≤ m < d;
• QSL.Exchange.ratio_le_explicit: 2 ‖E_d‖ / λ_d² ≤ (d - 1) / ((d - m) (1 - 1/m)²);
• QSL.Exchange.ratio_tendsto_one: 2 ‖E_d‖ / λ_d² → 1 (take m = ⌊√d⌋).

The sharp rate O(d^{-2/3}) (from the Plancherel–Rotach / Airy asymptotics of the zeros of He_d, DLMF 18.16.17) is not formalized; the elementary rate obtained here is weaker. The CZ-time bounds themselves are not formalized.

References

• P. Wocjan, M. Rötteler, D. Janzing, T. Beth, Simulating Hamiltonians in quantum networks: efficient schemes and complexity bounds, Phys. Rev. A 65 (2002) 042309.
• NIST Digital Library of Mathematical Functions, 18.16.17 (Hermite asymptotics).

theorem QSL.Exchange.sum_sq_mulVec_le {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m n ℝ) (x : n → ℝ) : ∑ i : m, A.mulVec x i ^ 2 ≤ ‖A‖ ^ 2 * ∑ j : n, x j ^ 2

Squared-norm form of Matrix.l2_opNorm_mulVec.

theorem QSL.Exchange.opNorm_le_of_sum_sq {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m n ℝ) {c : ℝ} (hc : 0 ≤ c) (h : ∀ (x : n → ℝ), ∑ i : m, A.mulVec x i ^ 2 ≤ c ^ 2 * ∑ j : n, x j ^ 2) : ‖A‖ ≤ c

A sufficient condition for an operator-norm bound, in squared form.

theorem QSL.Exchange.norm_kronecker_one_le {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (A : Matrix ι ι ℝ) : ‖Matrix.kroneckerMap (fun (x1 x2 : ℝ) => x1 * x2) A 1‖ ≤ ‖A‖

theorem QSL.Exchange.norm_one_kronecker_le {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (B : Matrix κ κ ℝ) : ‖Matrix.kroneckerMap (fun (x1 x2 : ℝ) => x1 * x2) 1 B‖ ≤ ‖B‖

theorem QSL.Exchange.norm_kronecker_le {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (A : Matrix ι ι ℝ) (B : Matrix κ κ ℝ) : ‖Matrix.kroneckerMap (fun (x1 x2 : ℝ) => x1 * x2) A B‖ ≤ ‖A‖ * ‖B‖

noncomputable def QSL.Exchange.bd (d : ℕ) : Matrix (Fin d) (Fin d) ℝ

The truncated annihilation operator on d levels: a e_j = √j e_{j-1}.

Equations

• QSL.Exchange.bd d = Matrix.of fun (i j : Fin d) => if ↑j = ↑i + 1 then √↑↑j else 0

noncomputable def QSL.Exchange.quad (d : ℕ) : Matrix (Fin d) (Fin d) ℝ

The quadrature Q = a + a†.

Equations

• QSL.Exchange.quad d = QSL.Exchange.bd d + (QSL.Exchange.bd d).transpose

noncomputable def QSL.Exchange.exch (d : ℕ) : Matrix (Fin d × Fin d) (Fin d × Fin d) ℝ

The exchange operator E = a† ⊗ a + a ⊗ a†.

Equations

• One or more equations did not get rendered due to their size.

Upper bound

theorem QSL.Exchange.bd_mulVec_apply {d : ℕ} (x : Fin d → ℝ) (i : Fin d) : (bd d).mulVec x i = if h : ↑i + 1 < d then √(↑↑i + 1) * x ⟨↑i + 1, h⟩ else 0

theorem QSL.Exchange.sum_sq_bd_mulVec_le {d : ℕ} (x : Fin d → ℝ) : ∑ i : Fin d, (bd d).mulVec x i ^ 2 ≤ (↑d - 1) * ∑ j : Fin d, x j ^ 2

theorem QSL.Exchange.norm_bd_le {d : ℕ} (hd : 1 ≤ d) : ‖bd d‖ ≤ √(↑d - 1)

theorem QSL.Exchange.exchange_norm_le {d : ℕ} (hd : 1 ≤ d) : ‖exch d‖ ≤ 2 * (↑d - 1)

The exchange operator has norm at most 2 (d - 1).

Lower bound

def QSL.Exchange.sq {d : ℕ} (x : Fin d → ℝ) : Fin d × Fin d → ℝ

The product vector x ⊗ x.

Equations

• QSL.Exchange.sq x p = x p.1 * x p.2

theorem QSL.Exchange.sum_sq_sq {d : ℕ} (x : Fin d → ℝ) : ∑ p : Fin d × Fin d, sq x p ^ 2 = (∑ i : Fin d, x i ^ 2) ^ 2

theorem QSL.Exchange.sq_dot_kronecker {d : ℕ} (M N : Matrix (Fin d) (Fin d) ℝ) (x : Fin d → ℝ) : sq x ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℝ) => x1 * x2) M N).mulVec (sq x) = x ⬝ᵥ M.mulVec x * x ⬝ᵥ N.mulVec x

theorem QSL.Exchange.dot_transpose_mulVec {d : ℕ} (M : Matrix (Fin d) (Fin d) ℝ) (x : Fin d → ℝ) : x ⬝ᵥ M.transpose.mulVec x = x ⬝ᵥ M.mulVec x

theorem QSL.Exchange.sq_dot_exch {d : ℕ} (x : Fin d → ℝ) : sq x ⬝ᵥ (exch d).mulVec (sq x) = 2 * (x ⬝ᵥ (bd d).mulVec x) ^ 2

The quadratic form of E on x ⊗ x is 2 (xᵀ a x)².

theorem QSL.Exchange.exchange_norm_ge {d : ℕ} (x : Fin d → ℝ) (hx : ∑ i : Fin d, x i ^ 2 = 1) (lam : ℝ) (hQ : (quad d).mulVec x = lam • x) : lam ^ 2 / 2 ≤ ‖exch d‖

Lower bound. If x is a real unit eigenvector of the quadrature Q = a + a† with eigenvalue lam, then ‖E‖ ≥ lam² / 2.

theorem QSL.Exchange.ratio_sandwich {d : ℕ} (hd : 1 ≤ d) (x : Fin d → ℝ) (hx : ∑ i : Fin d, x i ^ 2 = 1) (lam : ℝ) (hQ : (quad d).mulVec x = lam • x) (hlam : 0 < lam) : 1 ≤ 2 * ‖exch d‖ / lam ^ 2 ∧ 2 * ‖exch d‖ / lam ^ 2 ≤ 4 * (↑d - 1) / lam ^ 2

Sandwich of the ratio 2 κ / λ² between 1 and 4 (d - 1) / λ², κ = ‖E‖.

The largest eigenvalue and the variational fact

noncomputable def QSL.Exchange.quadLin (d : ℕ) : EuclideanSpace ℝ (Fin d) →ₗ[ℝ] EuclideanSpace ℝ (Fin d)

The quadrature as a linear map on Euclidean space.

Equations

• QSL.Exchange.quadLin d = Matrix.toEuclideanLin (QSL.Exchange.quad d)

theorem QSL.Exchange.quad_transpose (d : ℕ) : (quad d).transpose = quad d

theorem QSL.Exchange.quadLin_isSymmetric (d : ℕ) : (quadLin d).IsSymmetric

noncomputable def QSL.Exchange.lamMax (d : ℕ) : ℝ

The largest eigenvalue of the quadrature Q_d, as the supremum of its Rayleigh quotient.

Equations

• QSL.Exchange.lamMax d = ⨆ (x : { x : EuclideanSpace ℝ (Fin d) // x ≠ 0 }), RCLike.re (inner ℝ ((QSL.Exchange.quadLin d) ↑x) ↑x) / ‖↑x‖ ^ 2

theorem QSL.Exchange.inner_quadLin {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) : inner ℝ ((quadLin d) x) x = x.ofLp ⬝ᵥ (quad d).mulVec x.ofLp

theorem QSL.Exchange.norm_sq_euclid {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) : ‖x‖ ^ 2 = ∑ i : Fin d, x.ofLp i ^ 2

theorem QSL.Exchange.bddAbove_lamMax (d : ℕ) : BddAbove (Set.range fun (x : { x : EuclideanSpace ℝ (Fin d) // x ≠ 0 }) => RCLike.re (inner ℝ ((quadLin d) ↑x) ↑x) / ‖↑x‖ ^ 2)

theorem QSL.Exchange.quad_form_le_lamMax {d : ℕ} (v : Fin d → ℝ) : v ⬝ᵥ (quad d).mulVec v ≤ lamMax d * ∑ i : Fin d, v i ^ 2

Variational fact: ⟪v, Q v⟫ ≤ λ_d ‖v‖².

theorem QSL.Exchange.exists_unit_eigenvector {d : ℕ} (hd : 1 ≤ d) : ∃ (x : Fin d → ℝ), ∑ i : Fin d, x i ^ 2 = 1 ∧ (quad d).mulVec x = lamMax d • x

There is a unit eigenvector of Q_d with eigenvalue λ_d (d ≥ 1).

Uniform test vector on the last m levels

def QSL.Exchange.tail (d m : ℕ) : Fin d → ℝ

The indicator of the last m levels of the d-level ladder.

Equations

• QSL.Exchange.tail d m i = if d - m ≤ ↑i then 1 else 0

theorem QSL.Exchange.sum_sq_tail {d m : ℕ} (hm : m ≤ d) : ∑ i : Fin d, tail d m i ^ 2 = ↑m

theorem QSL.Exchange.tail_term_nonneg {d m : ℕ} (i : Fin d) : 0 ≤ tail d m i * (bd d).mulVec (tail d m) i

theorem QSL.Exchange.tail_term {d m : ℕ} (i : Fin d) : (if d - m ≤ ↑i ∧ ↑i + 1 < d then √↑(d - m) else 0) ≤ tail d m i * (bd d).mulVec (tail d m) i

theorem QSL.Exchange.sum_tail_term {d m : ℕ} (hm : 1 ≤ m) (hmd : m ≤ d) : (↑m - 1) * √(↑d - ↑m) ≤ tail d m ⬝ᵥ (bd d).mulVec (tail d m)

theorem QSL.Exchange.tail_quad_form {d : ℕ} (m : ℕ) : tail d m ⬝ᵥ (quad d).mulVec (tail d m) = 2 * tail d m ⬝ᵥ (bd d).mulVec (tail d m)

The quadratic form of Q on the test vector is 2 ⟪t, a t⟫.

theorem QSL.Exchange.lamMax_ge {d m : ℕ} (hm : 2 ≤ m) (hmd : m < d) : 2 * (1 - 1 / ↑m) * √(↑d - ↑m) ≤ lamMax d

Lower bound on the top eigenvalue: λ_d ≥ 2 (1 - 1/m) √(d - m), for 2 ≤ m < d.

Explicit bound and the limit

theorem QSL.Exchange.ratio_le_explicit {d m : ℕ} (hm : 2 ≤ m) (hmd : m < d) : 2 * ‖exch d‖ / lamMax d ^ 2 ≤ (↑d - 1) / ((↑d - ↑m) * (1 - 1 / ↑m) ^ 2)

Explicit upper bound of the ratio: 2 ‖E_d‖ / λ_d² ≤ (d - 1) / ((d - m) (1 - 1/m)²) for 2 ≤ m < d.

theorem QSL.Exchange.one_le_ratio {d : ℕ} (hd : 3 ≤ d) : 1 ≤ 2 * ‖exch d‖ / lamMax d ^ 2

The ratio is ≥ 1 once d ≥ 3 (so that λ_d > 0 by lamMax_ge).

theorem QSL.Exchange.ratio_tendsto_one : Filter.Tendsto (fun (d : ℕ) => 2 * ‖exch d‖ / lamMax d ^ 2) Filter.atTop (nhds 1)

Asymptotics. 2 ‖E_d‖ / λ_d² → 1, where λ_d is the largest eigenvalue of Q_d.