feat(PhyslibAlpha): Mandelstam–Tamm and Cramér–Rao in the open tight binding chain

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

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