Saturation of the Mandelstam–Tamm integral bound by fixed-axis two-level pulses

For a time-dependent Hamiltonian the integral form of the Mandelstam–Tamm bound (Mandelstam–Tamm 1945) reads arccos |⟨ψ(0), ψ(T)⟩| ≤ ∫₀ᵀ ΔE(t) dt (ℏ = 1). Here we show that it is an equality for every fixed-axis two-level pulse H(t) = f(t) σₓ / 2 with f ≥ 0, as long as the total rotation angle θ(T) = ∫₀ᵀ f is at most π.

The state is ψ = exp(−i θ σₓ / 2) |0⟩ = cos(θ/2) |0⟩ − i sin(θ/2) |1⟩; it depends on the pulse only through the accumulated angle θ(t) = ∫₀ᵗ f. Then ⟨σₓ⟩ = 0, so ΔE(t) = f(t)/2, ∫₀ᵀ ΔE = θ(T)/2 and |⟨ψ(0), ψ(T)⟩| = |cos(θ(T)/2)|.

Scope: the trajectory ψ(t) = qubitState (∫₀ᵗ f) is used as the evolution; for continuous f we prove (hasDerivAt_trajectory) that it solves the Schrödinger equation ψ′ = −i (f σₓ / 2) ψ with ψ(0) = |0⟩ (uniqueness is not proved). The statements without the Continuous f hypothesis are about the trajectory only.

Main results

• QSL.FixedAxis.energyStd_qubitState: ΔE = a/2 for H = (a/2) σₓ on every qubitState θ
• QSL.FixedAxis.arccos_overlap_qubitState: arccos ‖⟪ψ(0), ψ(θ)⟫‖ = θ/2 for 0 ≤ θ ≤ π
• QSL.FixedAxis.mandelstam_tamm_integral_eq: for f ≥ 0 with ∫₀ᵀ f ≤ π, ∫₀ᵀ ΔE(t) dt = arccos ‖⟪ψ(0), ψ(T)⟫‖
• QSL.FixedAxis.pi_pulse_quantum_speed_limit_ratio: for ∫₀ᵀ f = π the final state is orthogonal to the initial one and ∫₀ᵀ ΔE = π/2: the Mandelstam–Tamm ratio is exactly 1, whatever f
• QSL.FixedAxis.arccos_overlap_lt_of_pi_lt: strict inequality for π < θ < 3π

References

• L. Mandelstam, I. Tamm, The uncertainty relation between energy and time in non-relativistic quantum mechanics, J. Phys. USSR 9 (1945) 249–254.

@[reducible, inline]

abbrev QSL.FixedAxis.Vec2 : Type

Qubit vectors.

Equations

• QSL.FixedAxis.Vec2 = EuclideanSpace ℂ (Fin 2)

@[reducible, inline]

abbrev QSL.FixedAxis.Mat2 : Type

Single-qubit operators.

Equations

• QSL.FixedAxis.Mat2 = Matrix (Fin 2) (Fin 2) ℂ

def QSL.FixedAxis.sigmaX : Mat2

The Pauli matrix σₓ.

Equations

• QSL.FixedAxis.sigmaX = !![0, 1; 1, 0]

noncomputable def QSL.FixedAxis.hamX (a : ℝ) : Mat2

The Hamiltonian (a/2) σₓ.

Equations

• QSL.FixedAxis.hamX a = ↑(a / 2) • QSL.FixedAxis.sigmaX

def QSL.FixedAxis.act (M : Mat2) (v : Vec2) : Vec2

Action of a matrix on a vector.

Equations

• QSL.FixedAxis.act M v = WithLp.toLp 2 (Matrix.mulVec M v.ofLp)

def QSL.FixedAxis.qubitVec (c s : ℝ) : Vec2

The vector c |0⟩ − i s |1⟩ for real c, s.

Equations

• QSL.FixedAxis.qubitVec c s = !₂[↑c, -Complex.I * ↑s]

noncomputable def QSL.FixedAxis.qubitState (θ : ℝ) : Vec2

The state exp (−i θ σₓ / 2) |0⟩ = cos (θ/2) |0⟩ − i sin (θ/2) |1⟩.

Equations

• QSL.FixedAxis.qubitState θ = QSL.FixedAxis.qubitVec (Real.cos (θ / 2)) (Real.sin (θ / 2))

noncomputable def QSL.FixedAxis.expect (M : Mat2) (v : Vec2) : ℂ

Expectation value ⟨v, M v⟩.

Equations

• QSL.FixedAxis.expect M v = inner ℂ v (QSL.FixedAxis.act M v)

noncomputable def QSL.FixedAxis.energyStd (H : Mat2) (v : Vec2) : ℝ

Energy standard deviation ΔE = √(⟨H²⟩ − ⟨H⟩²) of the state v for the Hamiltonian H.

Equations

• QSL.FixedAxis.energyStd H v = √((QSL.FixedAxis.expect (H * H) v).re - (QSL.FixedAxis.expect H v).re ^ 2)

theorem QSL.FixedAxis.expect_sigmaX_qubitVec (c s : ℝ) : expect sigmaX (qubitVec c s) = 0

theorem QSL.FixedAxis.expect_sigmaX (θ : ℝ) : expect sigmaX (qubitState θ) = 0

theorem QSL.FixedAxis.norm_qubitState (θ : ℝ) : ‖qubitState θ‖ ^ 2 = 1

theorem QSL.FixedAxis.expect_sq (a θ : ℝ) : expect (hamX a * hamX a) (qubitState θ) = ↑((a / 2) ^ 2)

theorem QSL.FixedAxis.energyStd_qubitState (a θ : ℝ) (ha : 0 ≤ a) : energyStd (hamX a) (qubitState θ) = a / 2

Pointwise: for H = (a/2) σₓ the energy standard deviation of every state exp (−i θ σₓ / 2) |0⟩ equals |a|/2 (= a/2 for a ≥ 0).

theorem QSL.FixedAxis.inner_qubitState_zero (θ : ℝ) : inner ℂ (qubitState 0) (qubitState θ) = ↑(Real.cos (θ / 2))

The overlap ⟨ψ(0), ψ(θ)⟩ = cos (θ/2).

theorem QSL.FixedAxis.arccos_overlap_qubitState {θ : ℝ} (h0 : 0 ≤ θ) (hπ : θ ≤ Real.pi) : Real.arccos ‖inner ℂ (qubitState 0) (qubitState θ)‖ = θ / 2

Saturation, trajectory form: for 0 ≤ θ ≤ π, arccos ‖⟪ψ(0), ψ(θ)⟫‖ = θ/2.

theorem QSL.FixedAxis.arccos_overlap_lt_of_pi_lt {θ : ℝ} (h0 : Real.pi < θ) (h1 : θ < 3 * Real.pi) : Real.arccos ‖inner ℂ (qubitState 0) (qubitState θ)‖ < θ / 2

Strictness beyond a π pulse: for π < θ < 3π (so that the pulse overshoots), the bound is strict, arccos ‖⟪ψ(0), ψ(θ)⟫‖ < θ/2.

theorem QSL.FixedAxis.mandelstam_tamm_integral_eq {f : ℝ → ℝ} {T : ℝ} (hT : 0 ≤ T) (hf : ∀ t ∈ Set.Icc 0 T, 0 ≤ f t) (hπ : ∫ (t : ℝ) in 0..T, f t ≤ Real.pi) : ∫ (t : ℝ) in 0..T, energyStd (hamX (f t)) (qubitState (∫ (s : ℝ) in 0..t, f s)) = Real.arccos ‖inner ℂ (qubitState (∫ (s : ℝ) in 0..0, f s)) (qubitState (∫ (s : ℝ) in 0..T, f s))‖

Time-dependent form. For a pulse f ≥ 0 with θ(T) = ∫₀ᵀ f ≤ π, the trajectory ψ(t) = qubitState (∫₀ᵗ f) of H(t) = f(t) σₓ / 2 satisfies the Mandelstam–Tamm integral bound with equality: ∫₀ᵀ ΔE(t) dt = arccos ‖⟪ψ(0), ψ(T)⟫‖.

theorem QSL.FixedAxis.hasDerivAt_trajectory {f : ℝ → ℝ} (hf : Continuous f) (t : ℝ) : HasDerivAt (fun (t : ℝ) => qubitState (∫ (s : ℝ) in 0..t, f s)) (-Complex.I • act (hamX (f t)) (qubitState (∫ (s : ℝ) in 0..t, f s))) t

The trajectory solves the Schrödinger equation. For continuous f, the curve ψ(t) = qubitState (∫₀ᵗ f) satisfies ψ′(t) = −i H(t) ψ(t) with H(t) = f(t) σₓ / 2 (ℏ = 1).

theorem QSL.FixedAxis.mandelstam_tamm_integral_eq_solution {f : ℝ → ℝ} (hfc : Continuous f) {T : ℝ} (hT : 0 ≤ T) (hf : ∀ t ∈ Set.Icc 0 T, 0 ≤ f t) (hπ : ∫ (t : ℝ) in 0..T, f t ≤ Real.pi) : (∀ (t : ℝ), HasDerivAt (fun (t : ℝ) => qubitState (∫ (s : ℝ) in 0..t, f s)) (-Complex.I • act (hamX (f t)) (qubitState (∫ (s : ℝ) in 0..t, f s))) t) ∧ qubitState (∫ (s : ℝ) in 0..0, f s) = qubitState 0 ∧ ∫ (t : ℝ) in 0..T, energyStd (hamX (f t)) (qubitState (∫ (s : ℝ) in 0..t, f s)) = Real.arccos ‖inner ℂ (qubitState (∫ (s : ℝ) in 0..0, f s)) (qubitState (∫ (s : ℝ) in 0..T, f s))‖

Mandelstam–Tamm saturation for the Schrödinger solution. For continuous f ≥ 0 on [0,T] with ∫₀ᵀ f ≤ π, the curve ψ(t) = qubitState (∫₀ᵗ f) is a solution of ψ′ = −i (f σₓ/2) ψ with ψ(0) = |0⟩ (qubitState 0), and along it the Mandelstam–Tamm integral bound is an equality, ∫₀ᵀ ΔE(t) dt = arccos ‖⟪ψ(0), ψ(T)⟫‖. (Uniqueness of the solution is not proved; it is standard for linear ODEs.)

theorem QSL.FixedAxis.pi_pulse_quantum_speed_limit_ratio {f : ℝ → ℝ} {T : ℝ} (hT : 0 ≤ T) (hf : ∀ t ∈ Set.Icc 0 T, 0 ≤ f t) (hπ : ∫ (t : ℝ) in 0..T, f t = Real.pi) : inner ℂ (qubitState (∫ (s : ℝ) in 0..0, f s)) (qubitState (∫ (s : ℝ) in 0..T, f s)) = 0 ∧ ∫ (t : ℝ) in 0..T, energyStd (hamX (f t)) (qubitState (∫ (s : ℝ) in 0..t, f s)) = Real.pi / 2

Corollary (shape independence). If f ≥ 0 and ∫₀ᵀ f = π, the final state of the pulse is orthogonal to the initial state and ∫₀ᵀ ΔE = π/2: the Mandelstam–Tamm ratio (∫ΔE)/arccos|⟨ψ₀,ψ_T⟩| is exactly 1, for every shape f.