Documentation

Formalizations.Physics.QuantumMechanics.SpeedLimit.MargolusLevitin

The Margolus–Levitin quantum speed limit #

For a discrete spectral measure with populations pₙ ≥ 0, ∑ pₙ = 1, energies Eₙ ≥ 0 and mean energy ⟨E⟩ = ∑ pₙ Eₙ, if the autocorrelation S(τ) = ∑ pₙ e^{-i Eₙ τ} vanishes at τ ≥ 0, then π ≤ 2 ⟨E⟩ τ (units with ℏ = 1). Orthogonality is stated through the real and imaginary parts of S(τ), so the development is real.

Main results #

References #

The cosine inequality #

h(x) = cos x − 1 + (2/π)(x + sin x) ≥ 0 for x ≥ 0. The proof splits at x₀ = 2·arctan(2/π): h increases on [0, x₀], decreases on [x₀, π], with h(0) = h(π) = 0; for x ≥ π the linear term alone dominates since x + sin x is monotone.

theorem QSL.one_sub_le_cos {x : ℝ} (hx : 0 ≤ x) :

The Margolus–Levitin cosine inequality: 1 − (2/π)(x + sin x) ≤ cos x for x ≥ 0, with equality at x = 0 and x = π.

The Margolus–Levitin theorem #

theorem QSL.margolus_levitin {p E : ℕ → ℝ} {Ebar τ : ℝ} (hp : ∀ (n : ℕ), 0 ≤ p n) (hE : ∀ (n : ℕ), 0 ≤ E n) (hτ : 0 ≤ τ) (hsum : HasSum p 1) (hmean : HasSum (fun (n : ℕ) => p n * E n) Ebar) (hRe : HasSum (fun (n : ℕ) => p n * Real.cos (E n * τ)) 0) (hIm : HasSum (fun (n : ℕ) => p n * Real.sin (E n * τ)) 0) :
Real.pi ≤ 2 * Ebar * τ

The Margolus–Levitin theorem (1998), ℏ = 1: if a normalized population distribution p over nonnegative energies E has mean energy ⟨E⟩ and its autocorrelation S(τ) = ∑ pₙ·e^(−i·Eₙ·τ) vanishes at some time τ ≥ 0 (given here by its real and imaginary parts separately), then π ≤ 2·⟨E⟩·τ, i.e. the orthogonalization time obeys τ ≥ π/(2⟨E⟩).

This bounds the maximum number of distinct (mutually orthogonal) states any isolated physical system can pass through per unit time by 2⟨E⟩/π — the "clock speed of the universe" given an energy budget.