Documentation

Formalizations.Physics.QuantumMechanics.SpeedLimit.ApproxSpeedLimits

Robust (approximate) quantum speed limits #

The exact speed limits of QuditEntangling and GateEigenphases assume that the target state is reached exactly. Here the target is reached only up to a state infidelity ε. Everything follows from the triangle inequality for the Fubini–Study angle fsAngle u v = arccos ‖⟪u, v⟫‖: a state of fidelity ≥ 1 − ε with a target lies at angle ≤ arccos √(1 − ε) = arcsin √ε from it.

Here ε is the infidelity of one specific input/output pair of states, ‖⟪target, U ψ⟫‖² ≥ 1 − ε. It is not an average gate infidelity (which would need an average over inputs).

The statements were suggested by an external review.

Main results #

Tightness (not formalized): with H = (Ω/2) σₓ, ψ₀ = e₀, ψ₁ = e₁, the transfer probability is P₁(T) = sin² (Ω T / 2), so for ε = cos² (Ω T / 2) the bound 2 arccos √ε = Ω T is attained.

References #

theorem QSL.Qudit.fsAngle_le_arcsin_sqrt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {u v : E} {ε : ℝ} (hε : 0 ≤ ε) (h : 1 - ε ≤ ‖inner ℂ u v‖ ^ 2) :

A pair of vectors with ‖⟪u, v⟫‖² ≥ 1 − ε lies at Fubini–Study angle ≤ arcsin √ε.

theorem QSL.Qudit.norm_inner_le_cos_of_angle {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {T Φ p : E} (hT : ‖T‖ = 1) (hΦ : ‖Φ‖ = 1) (hp : ‖p‖ = 1) {θ : ℝ} (hθ : θ < Real.pi / 4) (hTΦ : fsAngle T Φ ≤ θ) (hTp : Real.pi / 4 ≤ fsAngle T p) :

If Φ is within angle θ < π/4 of a target T, and T is at angle ≥ π/4 from p, then Φ has overlap at most cos (π/4 − θ) with the unit vector p.

theorem QSL.Qudit.norm_bellPair {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] {i₀ i₁ : ι} {j₀ j₁ : κ} (hi : i₀ ≠ i₁) :
‖bellPair i₀ i₁ j₀ j₁‖ = 1
theorem QSL.Qudit.pi_div_four_sub_le_entangling_time_approx {ι : 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₁) (Φ : EuclideanSpace ℂ (ι × κ)) (hΦ : ‖Φ‖ = 1) (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) = Φ) {ε : ℝ} (hε : 0 ≤ ε) (hfid : 1 - ε ≤ ‖inner ℂ (bellPair i₀ i₁ j₀ j₁) Φ‖ ^ 2) :

Robust Bell-pair entangling time. Let H be a Hermitian interaction with ‖H‖ ≤ J and U = ∏ₖ exp (−i τₖ (Aₖ ⊗ 1 + 1 ⊗ Bₖ + H)) with arbitrary Hermitian local controls. If U maps a unit product vector to a unit vector Φ whose state infidelity with the two-level Bell vector is at most ε, i.e. ‖⟪Bell, Φ⟫‖² ≥ 1 − ε, then π/4 − arcsin √ε ≤ J · ∑ τₖ. Here ε is the infidelity of this one input/output pair, not an average gate infidelity. For ε = 0 this is pi_div_four_le_entangling_time (Dür et al. 2001).

theorem QSL.Qudit.pi_div_four_sub_le_entangling_time_shift_approx {ι : 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₁) (Φ : EuclideanSpace ℂ (ι × κ)) (hΦ : ‖Φ‖ = 1) (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) = Φ) {ε : ℝ} (hε : 0 ≤ ε) (hfid : 1 - ε ≤ ‖inner ℂ (bellPair i₀ i₁ j₀ j₁) Φ‖ ^ 2) :

Robust Bell-pair entangling time, shifted coupling. As pi_div_four_sub_le_entangling_time_approx, with ‖H − c • 1‖ ≤ J for some real c.

theorem QSL.Gate.two_arccos_sqrt_le_time_approx {n : Type u_1} [Fintype n] [DecidableEq n] (Ω : ℝ) (steps : List (ℝ × ℝ × Matrix n n ℂ)) (hτ : ∀ s ∈ steps, 0 ≤ s.1) (hH : ∀ s ∈ steps, s.2.2.IsHermitian) (hΩ : ∀ s ∈ steps, ‖s.2.2 - ↑s.2.1 • 1‖ ≤ Ω / 2) (ψ₀ ψ₁ ψ : EuclideanSpace ℂ n) (h₀ : ‖ψ₀‖ = 1) (h₁ : ‖ψ₁‖ = 1) (hψ : ‖ψ‖ = 1) (horth : inner ℂ ψ₁ ψ₀ = 0) (hU : TwoQubit.act (List.map (fun (s : ℝ × ℝ × Matrix n n ℂ) => NormedSpace.exp ((-↑s.1 * Complex.I) • s.2.2)) steps).prod ψ₀ = ψ) {ε : ℝ} (hε : 0 ≤ ε) (hfid : 1 - ε ≤ ‖inner ℂ ψ₁ ψ‖ ^ 2) :

Robust state-transfer time. Let U = ∏ₖ exp (−i τₖ Hₖ) with τₖ ≥ 0, Hₖ Hermitian and ‖Hₖ − cₖ • 1‖ ≤ Ω / 2. If ψ₀ ⊥ ψ₁ are unit vectors and U ψ₀ = ψ is a unit vector with state infidelity at most ε relative to ψ₁, i.e. ‖⟪ψ₁, ψ⟫‖² ≥ 1 − ε, then 2 · arccos √ε ≤ Ω · ∑ τₖ. Here ε is the infidelity of this one input/output pair, not an average gate infidelity. (Tight: H = (Ω/2) σₓ gives P₁(T) = sin² (Ω T / 2).)