The entangling time with the spectral half-width of the interaction

The interaction H of QSL.Qudit.arccos_le_entangling_time is only defined up to a multiple of the identity: c • 1 = (c • 1) ⊗ 1 is a local term, and can be absorbed into the local control Aₖ. Hence the bound arccos λ ≤ J · ∑ τₖ holds with J any bound of the shifted norm ‖H − c • 1‖, c real. For H Hermitian with spectrum in [m, M] the choice c = (m + M) / 2 gives the spectral half-width (M − m) / 2 (this spectral fact is taken as a hypothesis here, not proved).

For the two-qubit Heisenberg interaction H = XX + YY + ZZ (spectrum {1, −3}), H + 1 = 2 · SWAP, so ‖H − (−1) • 1‖ = 2 instead of ‖H‖ = 3. The Bell vector then needs total time T ≥ π / 8. This matches the Heisenberg entangling time π / 8 of Dür, Vidal, Cirac, Linden and Popescu; that this time is achievable is their result and is not formalized here.

Main results

• QSL.Qudit.arccos_le_entangling_time_shift: arccos λ ≤ J · ∑ τₖ whenever ‖H − c • 1‖ ≤ J
• QSL.Qudit.arccos_le_entangling_time_halfWidth: the spectral half-width version
• QSL.Qudit.pi_div_four_le_entangling_time_shift: Bell vector, π / 4 ≤ J · ∑ τₖ
• QSL.Qudit.pi_div_four_le_entangling_time_local, QSL.Qudit.pi_div_four_le_entangling_time_shift_local: the same when the target is (P ⊗ Q) · bellPair with P, Q unitary (any gate locally equivalent to CNOT, e.g. IBM's ECR)
• QSL.Qudit.heisenberg_shift_norm: ‖heisenberg − (−1) • 1‖ = 2
• QSL.Qudit.pi_div_eight_le_heisenberg_time: Bell vector under the Heisenberg interaction needs ∑ τₖ ≥ π / 8

References

• W. Dür, G. Vidal, J. I. Cirac, N. Linden, S. Popescu, Entanglement capabilities of nonlocal Hamiltonians, Phys. Rev. Lett. 87 (2001) 137901.

theorem QSL.Qudit.arccos_le_entangling_time_shift {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (H : Matrix (ι × κ) (ι × κ) ℂ) (hH : H.IsHermitian) (c J : ℝ) (hJ : ‖H - ↑c • 1‖ ≤ J) (steps : List (ℝ × Matrix ι ι ℂ × Matrix κ κ ℂ)) (hτ : ∀ s ∈ steps, 0 ≤ s.1) (hA : ∀ s ∈ steps, s.2.1.IsHermitian) (hB : ∀ s ∈ steps, s.2.2.IsHermitian) (a : EuclideanSpace ℂ ι) (b : EuclideanSpace ℂ κ) (ha : ‖a‖ = 1) (hb : ‖b‖ = 1) (Φ : EuclideanSpace ℂ (ι × κ)) (hU : TwoQubit.act (List.map (fun (s : ℝ × Matrix ι ι ℂ × Matrix κ κ ℂ) => NormedSpace.exp ((-↑s.1 * Complex.I) • (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) s.2.1 1 + Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 s.2.2 + H))) steps).prod (prodVec a b) = Φ) (lam : ℝ) (hlam : ∀ (x : EuclideanSpace ℂ ι) (y : EuclideanSpace ℂ κ), ‖x‖ = 1 → ‖y‖ = 1 → ‖inner ℂ Φ (prodVec x y)‖ ≤ lam) : Real.arccos lam ≤ J * (List.map Prod.fst steps).sum

(C, shifted) Entangling-time bound with a shifted interaction. As arccos_le_entangling_time, but with ‖H − c • 1‖ ≤ J for some real c in place of ‖H‖ ≤ J. The identity part of H is a local term and is absorbed into the control.

theorem QSL.Qudit.arccos_le_entangling_time_halfWidth {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (H : Matrix (ι × κ) (ι × κ) ℂ) (hH : H.IsHermitian) (m M : ℝ) (hspec : ‖H - ↑((m + M) / 2) • 1‖ ≤ (M - m) / 2) (steps : List (ℝ × Matrix ι ι ℂ × Matrix κ κ ℂ)) (hτ : ∀ s ∈ steps, 0 ≤ s.1) (hA : ∀ s ∈ steps, s.2.1.IsHermitian) (hB : ∀ s ∈ steps, s.2.2.IsHermitian) (a : EuclideanSpace ℂ ι) (b : EuclideanSpace ℂ κ) (ha : ‖a‖ = 1) (hb : ‖b‖ = 1) (Φ : EuclideanSpace ℂ (ι × κ)) (hU : TwoQubit.act (List.map (fun (s : ℝ × Matrix ι ι ℂ × Matrix κ κ ℂ) => NormedSpace.exp ((-↑s.1 * Complex.I) • (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) s.2.1 1 + Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 s.2.2 + H))) steps).prod (prodVec a b) = Φ) (lam : ℝ) (hlam : ∀ (x : EuclideanSpace ℂ ι) (y : EuclideanSpace ℂ κ), ‖x‖ = 1 → ‖y‖ = 1 → ‖inner ℂ Φ (prodVec x y)‖ ≤ lam) : Real.arccos lam ≤ (M - m) / 2 * (List.map Prod.fst steps).sum

(C, spectral half-width) If ‖H − ((m + M)/2) • 1‖ ≤ (M − m)/2 — which holds for Hermitian H with all eigenvalues in [m, M]; this spectral fact is taken as a hypothesis — then arccos λ ≤ ((M − m)/2) · ∑ τₖ. For the Heisenberg interaction XX + YY + ZZ (spectrum {1, −3}) the half-width is 2, versus ‖H‖ = 3.

theorem QSL.Qudit.pi_div_four_le_entangling_time_shift {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (H : Matrix (ι × κ) (ι × κ) ℂ) (hH : H.IsHermitian) (c J : ℝ) (hJ : ‖H - ↑c • 1‖ ≤ J) (steps : List (ℝ × Matrix ι ι ℂ × Matrix κ κ ℂ)) (hτ : ∀ s ∈ steps, 0 ≤ s.1) (hA : ∀ s ∈ steps, s.2.1.IsHermitian) (hB : ∀ s ∈ steps, s.2.2.IsHermitian) (a : EuclideanSpace ℂ ι) (b : EuclideanSpace ℂ κ) (ha : ‖a‖ = 1) (hb : ‖b‖ = 1) {i₀ i₁ : ι} {j₀ j₁ : κ} (hi : i₀ ≠ i₁) (hj : j₀ ≠ j₁) (hU : TwoQubit.act (List.map (fun (s : ℝ × Matrix ι ι ℂ × Matrix κ κ ℂ) => NormedSpace.exp ((-↑s.1 * Complex.I) • (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) s.2.1 1 + Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 s.2.2 + H))) steps).prod (prodVec a b) = bellPair i₀ i₁ j₀ j₁) : Real.pi / 4 ≤ J * (List.map Prod.fst steps).sum

(D, shifted) Bell vector: with ‖H − c • 1‖ ≤ J, preparing (e_{i₀ j₀} + e_{i₁ j₁}) / √2 from a unit product vector takes J · ∑ τₖ ≥ π / 4.

Targets locally equivalent to the Bell vector

theorem QSL.Qudit.norm_inner_act_kronecker_prodVec_le {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] {P : Matrix ι ι ℂ} {Q : Matrix κ κ ℂ} (hP : P ∈ Matrix.unitaryGroup ι ℂ) (hQ : Q ∈ Matrix.unitaryGroup κ ℂ) (Φ : EuclideanSpace ℂ (ι × κ)) (lam : ℝ) (hlam : ∀ (x : EuclideanSpace ℂ ι) (y : EuclideanSpace ℂ κ), ‖x‖ = 1 → ‖y‖ = 1 → ‖inner ℂ Φ (prodVec x y)‖ ≤ lam) (x : EuclideanSpace ℂ ι) (y : EuclideanSpace ℂ κ) (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : ‖inner ℂ (TwoQubit.act (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P Q) Φ) (prodVec x y)‖ ≤ lam

Local unitaries do not change the overlap bound with unit product vectors: if every unit product vector has overlap at most lam with Φ, the same holds for (P ⊗ Q) Φ.

theorem QSL.Qudit.pi_div_four_le_entangling_time_local {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (H : Matrix (ι × κ) (ι × κ) ℂ) (hH : H.IsHermitian) (J : ℝ) (hJ : ‖H‖ ≤ J) (steps : List (ℝ × Matrix ι ι ℂ × Matrix κ κ ℂ)) (hτ : ∀ s ∈ steps, 0 ≤ s.1) (hA : ∀ s ∈ steps, s.2.1.IsHermitian) (hB : ∀ s ∈ steps, s.2.2.IsHermitian) (a : EuclideanSpace ℂ ι) (b : EuclideanSpace ℂ κ) (ha : ‖a‖ = 1) (hb : ‖b‖ = 1) {i₀ i₁ : ι} {j₀ j₁ : κ} (hi : i₀ ≠ i₁) (hj : j₀ ≠ j₁) {P : Matrix ι ι ℂ} {Q : Matrix κ κ ℂ} (hP : P ∈ Matrix.unitaryGroup ι ℂ) (hQ : Q ∈ Matrix.unitaryGroup κ ℂ) (hU : TwoQubit.act (List.map (fun (s : ℝ × Matrix ι ι ℂ × Matrix κ κ ℂ) => NormedSpace.exp ((-↑s.1 * Complex.I) • (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) s.2.1 1 + Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 s.2.2 + H))) steps).prod (prodVec a b) = TwoQubit.act (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P Q) (bellPair i₀ i₁ j₀ j₁)) : Real.pi / 4 ≤ J * (List.map Prod.fst steps).sum

(D, local) Bell vector up to local unitaries: if the evolution maps a unit product vector to (P ⊗ Q) · bellPair with P, Q unitary, then π / 4 ≤ J · ∑ τₖ.

This applies to every two-qubit gate locally equivalent to CNOT on the qubit subspace, e.g. IBM's echoed cross-resonance gate ECR = (local) · CNOT · (local): such a gate maps some product state to a local unitary applied to a Bell state, hence needs J · T ≥ π / 4. (The ECR matrix itself is not formalized.)

theorem QSL.Qudit.pi_div_four_le_entangling_time_shift_local {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (H : Matrix (ι × κ) (ι × κ) ℂ) (hH : H.IsHermitian) (c J : ℝ) (hJ : ‖H - ↑c • 1‖ ≤ J) (steps : List (ℝ × Matrix ι ι ℂ × Matrix κ κ ℂ)) (hτ : ∀ s ∈ steps, 0 ≤ s.1) (hA : ∀ s ∈ steps, s.2.1.IsHermitian) (hB : ∀ s ∈ steps, s.2.2.IsHermitian) (a : EuclideanSpace ℂ ι) (b : EuclideanSpace ℂ κ) (ha : ‖a‖ = 1) (hb : ‖b‖ = 1) {i₀ i₁ : ι} {j₀ j₁ : κ} (hi : i₀ ≠ i₁) (hj : j₀ ≠ j₁) {P : Matrix ι ι ℂ} {Q : Matrix κ κ ℂ} (hP : P ∈ Matrix.unitaryGroup ι ℂ) (hQ : Q ∈ Matrix.unitaryGroup κ ℂ) (hU : TwoQubit.act (List.map (fun (s : ℝ × Matrix ι ι ℂ × Matrix κ κ ℂ) => NormedSpace.exp ((-↑s.1 * Complex.I) • (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) s.2.1 1 + Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 s.2.2 + H))) steps).prod (prodVec a b) = TwoQubit.act (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P Q) (bellPair i₀ i₁ j₀ j₁)) : Real.pi / 4 ≤ J * (List.map Prod.fst steps).sum

(D, local, shifted) As pi_div_four_le_entangling_time_local, with ‖H − c • 1‖ ≤ J.

The two-qubit Heisenberg interaction

def QSL.Qudit.pauliX : Matrix (Fin 2) (Fin 2) ℂ

The Pauli matrix X.

Equations

• QSL.Qudit.pauliX = !![0, 1; 1, 0]

def QSL.Qudit.pauliY : Matrix (Fin 2) (Fin 2) ℂ

The Pauli matrix Y.

Equations

• QSL.Qudit.pauliY = !![0, -Complex.I; Complex.I, 0]

def QSL.Qudit.pauliZ : Matrix (Fin 2) (Fin 2) ℂ

The Pauli matrix Z.

Equations

• QSL.Qudit.pauliZ = !![1, 0; 0, -1]

def QSL.Qudit.heisenberg : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ

The Heisenberg interaction X ⊗ X + Y ⊗ Y + Z ⊗ Z on two qubits.

Equations

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

theorem QSL.Qudit.heisenberg_isHermitian : heisenberg.IsHermitian

theorem QSL.Qudit.heisenberg_shift_norm : ‖heisenberg - ↑(-1) • 1‖ = 2

‖XX + YY + ZZ − (−1) • 1‖ = 2 (the spectral half-width), whereas ‖XX + YY + ZZ‖ = 3.

theorem QSL.Qudit.pi_div_eight_le_heisenberg_time (steps : List (ℝ × Matrix (Fin 2) (Fin 2) ℂ × Matrix (Fin 2) (Fin 2) ℂ)) (hτ : ∀ s ∈ steps, 0 ≤ s.1) (hA : ∀ s ∈ steps, s.2.1.IsHermitian) (hB : ∀ s ∈ steps, s.2.2.IsHermitian) (a b : EuclideanSpace ℂ (Fin 2)) (ha : ‖a‖ = 1) (hb : ‖b‖ = 1) (hU : TwoQubit.act (List.map (fun (s : ℝ × Matrix (Fin 2) (Fin 2) ℂ × Matrix (Fin 2) (Fin 2) ℂ) => NormedSpace.exp ((-↑s.1 * Complex.I) • (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) s.2.1 1 + Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 s.2.2 + heisenberg))) steps).prod (prodVec a b) = bellPair 0 1 0 1) : Real.pi / 8 ≤ (List.map Prod.fst steps).sum

Bell vector under the Heisenberg interaction with arbitrary local control (two qubits, no ancilla): the total time is at least π / 8. Dür–Vidal–Cirac–Linden–Popescu (2001) show that π / 8 is achievable for this interaction; only the lower bound is proved here.