From 11b367b7cfe4e50945e346ee7a73bde3ac3f7b97 Mon Sep 17 00:00:00 2001 From: Eduardo Nava Hernandez Date: Tue, 29 Sep 2026 17:23:34 -0600 Subject: [PATCH] =?UTF-8?q?feat(PhyslibAlpha):=20Mandelstam=E2=80=93Tamm?= =?UTF-8?q?=20and=20Cram=C3=A9r=E2=80=93Rao=20in=20the=20open=20tight=20bi?= =?UTF-8?q?nding=20chain?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- PhyslibAlpha.lean | 1 + .../TightBindingChain/MandelstamTamm.lean | 140 ++++++++++++++++++ 2 files changed, 141 insertions(+) create mode 100644 PhyslibAlpha/CondensedMatter/TightBindingChain/MandelstamTamm.lean diff --git a/PhyslibAlpha.lean b/PhyslibAlpha.lean index 4d389b646..7f8f019fd 100644 --- a/PhyslibAlpha.lean +++ b/PhyslibAlpha.lean @@ -35,6 +35,7 @@ public import PhyslibAlpha.ClassicalMechanics.NortonDome.Solution public import PhyslibAlpha.ClassicalMechanics.NortonDome.Sqrt public import PhyslibAlpha.CondensedMatter.TightBindingChain.Current public import PhyslibAlpha.CondensedMatter.TightBindingChain.CurrentEigenstates +public import PhyslibAlpha.CondensedMatter.TightBindingChain.MandelstamTamm public import PhyslibAlpha.CondensedMatter.TightBindingChain.MaxCurrentState public import PhyslibAlpha.CondensedMatter.TightBindingChain.OpenBoundary public import PhyslibAlpha.CondensedMatter.TightBindingChain.Uncertainty diff --git a/PhyslibAlpha/CondensedMatter/TightBindingChain/MandelstamTamm.lean b/PhyslibAlpha/CondensedMatter/TightBindingChain/MandelstamTamm.lean new file mode 100644 index 000000000..0ff8810c8 --- /dev/null +++ b/PhyslibAlpha/CondensedMatter/TightBindingChain/MandelstamTamm.lean @@ -0,0 +1,140 @@ +/- +Copyright (c) 2026 Eduardo Nava-Hernandez. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Eduardo Nava-Hernandez +-/ +module + +public import PhyslibAlpha.CondensedMatter.TightBindingChain.Current +public import PhyslibAlpha.CondensedMatter.TightBindingChain.Uncertainty +/-! + +# Mandelstam–Tamm and Cramér–Rao in the open tight binding chain + +## i. Overview + +The bracket `⁅H, X⁆ = -(i/2) (H X - X H)` is `-J / 2`, with `J = i (H X - X H)` the current, the +velocity `d⟨X⟩/dt`. The energy–position uncertainty relation therefore reads in two ways: + +* **Mandelstam–Tamm**: `|⟨J⟩| ≤ 2 ΔH ΔX`, the position moves no faster than the energy spread + allows; +* **quantum Cramér–Rao**: the error-propagation Fisher information `⟨J⟩² / Var X` of the position, + for a displacement generated by `H`, is at most `4 Var H`, the quantum Fisher information of a + pure state. + +Both are the single statement `⟨J⟩² ≤ 4 Var H · Var X`, that is `mandelstamTammRatio ≤ 1`. + +## ii. Key results + +- `currentObservable` : the current `J` as an observable. +- `coe_bracket_openHamiltonian_position` : `⁅H, X⁆ = -J / 2`. +- `sq_expectation_current_le` : `⟨J⟩² ≤ 4 Var H · Var X`. +- `mandelstam_tamm` : `|⟨J⟩| ≤ 2 ΔH ΔX`. +- `cramer_rao` : `⟨J⟩² / Var X ≤ 4 Var H`. +- `mandelstamTammRatio` : `⟨J⟩² / (4 Var H · Var X)`, at most one by + `mandelstamTammRatio_le_one`. + +## iii. Table of contents + +- A. The current as an observable +- B. Mandelstam–Tamm and Cramér–Rao + +## iv. References + +* https://www.damtp.cam.ac.uk/user/tong/aqm/aqmtwo.pdf. [ref: tong_statistical_physics] +-/ + +@[expose] public section + +open scoped ComplexOrder InnerProductSpace selfAdjoint +open ProbabilisticTheory +open ContinuousLinearMap UnitalPositiveLinearMap + +namespace CondensedMatter +namespace TightBindingChain +variable (T : TightBindingChain) + +/-! + +## A. The current as an observable + +-/ + +/-- The current `J = i (H X - X H)` as an observable. -/ +noncomputable abbrev currentObservable := T.toObservable T.current T.current_hermitian + +/-- The bracket of the Hamiltonian and the position is minus half the current: +`⁅H, X⁆ = -J / 2`. -/ +lemma coe_bracket_openHamiltonian_position : + ((⁅T.openHamiltonianObservable, T.positionObservable⁆ : Observable _) : + T.HilbertSpace →L[ℂ] T.HilbertSpace) = + (-(1 / 2) : ℂ) • (T.currentObservable : T.HilbertSpace →L[ℂ] T.HilbertSpace) := by + refine ContinuousLinearMap.ext fun ψ => ?_ + rw [selfAdjoint.coe_bracket, smul_apply, smul_apply] + change -(Complex.I / 2) • (T.openHamiltonian (T.position ψ) - T.position (T.openHamiltonian ψ)) = + (-(1 / 2) : ℂ) • T.current ψ + rw [current, LinearMap.smul_apply, LinearMap.sub_apply, LinearMap.comp_apply, + LinearMap.comp_apply, smul_smul] + congr 1 + ring + +/-- The expected bracket is minus half the expected current. -/ +lemma expectation_bracket_openHamiltonian_position + (ω : 𝓢[ℂ, T.HilbertSpace →L[ℂ] T.HilbertSpace]) : + ω⟨⁅T.openHamiltonianObservable, T.positionObservable⁆⟩ = -(ω⟨T.currentObservable⟩ / 2) := by + apply Complex.ofReal_injective + rw [← apply_observable_eq_expectation, coe_bracket_openHamiltonian_position, map_smul, + apply_observable_eq_expectation, smul_eq_mul] + push_cast + ring + +/-! + +## B. Mandelstam–Tamm and Cramér–Rao + +-/ + +variable (ω : 𝓢[ℂ, T.HilbertSpace →L[ℂ] T.HilbertSpace]) + +/-- In every state, `⟨J⟩² ≤ 4 Var H · Var X`. -/ +lemma sq_expectation_current_le : + ω⟨T.currentObservable⟩ ^ 2 ≤ + 4 * (variance ω T.openHamiltonianObservable * variance ω T.positionObservable) := by + have h := T.robertson_schrodinger_openHamiltonian_position ω + rw [expectation_bracket_openHamiltonian_position] at h + nlinarith [sq_nonneg (covariance ω T.openHamiltonianObservable T.positionObservable)] + +/-- **Mandelstam–Tamm.** The position moves no faster than the energy spread allows: +`|d⟨X⟩/dt| = |⟨J⟩| ≤ 2 ΔH ΔX`. -/ +theorem mandelstam_tamm : + |ω⟨T.currentObservable⟩| ≤ + 2 * (√(variance ω T.openHamiltonianObservable) * √(variance ω T.positionObservable)) := by + rw [← Real.sqrt_mul (variance_nonneg ω _), ← Real.sqrt_sq_eq_abs, + show (2 : ℝ) = √(2 ^ 2) by rw [Real.sqrt_sq two_pos.le], ← Real.sqrt_mul (by positivity)] + exact Real.sqrt_le_sqrt (by linarith [T.sq_expectation_current_le ω]) + +/-- **Quantum Cramér–Rao.** For a displacement generated by `H`, the error-propagation Fisher +information `⟨J⟩² / Var X` of the position is at most `4 Var H`, the quantum Fisher information +of a pure state. -/ +theorem cramer_rao : + ω⟨T.currentObservable⟩ ^ 2 / variance ω T.positionObservable ≤ + 4 * variance ω T.openHamiltonianObservable := by + rcases (variance_nonneg ω T.positionObservable).eq_or_lt with h | h + · rw [← h, div_zero] + exact mul_nonneg four_pos.le (variance_nonneg ω _) + · rw [div_le_iff₀ h] + linarith [T.sq_expectation_current_le ω] + +/-- The Mandelstam–Tamm ratio `⟨J⟩² / (4 Var H · Var X)`: how close a state comes to both +Mandelstam–Tamm and Cramér–Rao. -/ +noncomputable def mandelstamTammRatio : ℝ := + ω⟨T.currentObservable⟩ ^ 2 / + (4 * (variance ω T.openHamiltonianObservable * variance ω T.positionObservable)) + +/-- The Mandelstam–Tamm ratio never exceeds one. -/ +lemma mandelstamTammRatio_le_one : T.mandelstamTammRatio ω ≤ 1 := + div_le_one_of_le₀ (T.sq_expectation_current_le ω) + (mul_nonneg four_pos.le (mul_nonneg (variance_nonneg ω _) (variance_nonneg ω _))) + +end TightBindingChain +end CondensedMatter