A Mandelstam–Tamm speed limit in L¹ form

With the notation of MargolusLevitin, if the autocorrelation vanishes at τ ≥ 0 then 1 ≤ D₁ τ, where D₁ = ∑ pₙ |Eₙ - ⟨E⟩| is the mean absolute deviation of the energy (ℏ = 1).

The centered autocorrelation g(t) = e^{i⟨E⟩t} S(t) goes from g(0) = 1 to g(τ) = 0 with speed ‖g′‖ ≤ D₁. Since D₁ ≤ ΔE by the Cauchy–Schwarz inequality, this implies the weak form τ ≥ 1/ΔE of the Mandelstam–Tamm bound τ ≥ π/(2ΔE), which is not proved here.

Main results

• QSL.mandelstam_tamm_L1: 1 ≤ D₁ τ.
• QSL.l1_dev_le_sqrt_variance, QSL.mandelstam_tamm_weak: D₁ ≤ ΔE, hence 1 ≤ ΔE τ.

References

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

theorem QSL.mandelstam_tamm_L1 {p E : ℕ → ℝ} {Ebar D1 τ : ℝ} (hp : ∀ (n : ℕ), 0 ≤ p n) (hτ : 0 ≤ τ) (hsum : HasSum p 1) (hdev : HasSum (fun (n : ℕ) => p n * |E n - Ebar|) D1) (horth : HasSum (fun (n : ℕ) => ↑(p n) * Complex.exp (↑(-(E n * τ)) * Complex.I)) 0) : 1 ≤ D1 * τ

Mandelstam–Tamm-type speed limit, L¹ form (ℏ = 1): if a normalized population distribution p over energies E has mean absolute energy deviation D₁ = ∑ pₙ·|Eₙ − Ebar| around any reference energy Ebar, and the autocorrelation S(τ) = ∑ pₙ·e^{−i·Eₙ·τ} vanishes at some τ ≥ 0, then 1 ≤ D₁·τ, i.e. τ ≥ 1/D₁. With Ebar = ⟨E⟩ and Cauchy–Schwarz this implies the textbook weak Mandelstam–Tamm bound τ ≥ 1/ΔE.

theorem QSL.l1_dev_le_sqrt_variance {p E : ℕ → ℝ} {Ebar D1 V : ℝ} (hp : ∀ (n : ℕ), 0 ≤ p n) (hsum : HasSum p 1) (hdev : HasSum (fun (n : ℕ) => p n * |E n - Ebar|) D1) (hvar : HasSum (fun (n : ℕ) => p n * (E n - Ebar) ^ 2) V) : D1 ≤ √V

Cauchy–Schwarz for a probability distribution: the mean absolute deviation is at most the standard deviation, D₁ ≤ √(∑ pₙ (Eₙ − Ē)²) (from ∑ pₙ (|Eₙ − Ē| − D₁)² ≥ 0).

theorem QSL.mandelstam_tamm_weak {p E : ℕ → ℝ} {Ebar V τ : ℝ} (hp : ∀ (n : ℕ), 0 ≤ p n) (hτ : 0 ≤ τ) (hsum : HasSum p 1) (hdev : Summable fun (n : ℕ) => p n * |E n - Ebar|) (hvar : HasSum (fun (n : ℕ) => p n * (E n - Ebar) ^ 2) V) (horth : HasSum (fun (n : ℕ) => ↑(p n) * Complex.exp (↑(-(E n * τ)) * Complex.I)) 0) : 1 ≤ √V * τ

The textbook weak Mandelstam–Tamm bound (ℏ = 1): τ ≥ 1/ΔE, from the L¹ form and D₁ ≤ ΔE.