refactor(PhyslibAlpha): state the open chain uncertainty on its own Hilbert space

PhyslibAlpha/CondensedMatter/TightBindingChain/Uncertainty.lean

@@ -7,21 +7,21 @@ module
 
 public import PhyslibAlpha.CondensedMatter.TightBindingChain.OpenBoundary
 public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.State.VectorUncertainty
+public import PhyslibAlpha.QuantumMechanics.HilbertSpaces.FiniteTarget.Operators
 
 /-!
 
 # Energy–position uncertainty in the open tight binding chain
 
 The Hamiltonian and the position operator of the tight binding chain with open boundary
-conditions, acting on the site amplitudes in `ℂ^N`, are observables of the C⋆-algebra of
-operators on `ℂ^N`. The
-Robertson–Schrödinger relation then bounds their spreads in every state by the expected
+conditions are observables of the C⋆-algebra of operators on the Hilbert space of the chain.
+The Robertson–Schrödinger relation then bounds their spreads in every state by the expected
 bracket `⁅H, X⁆ = -(i/2) (H X - X H)`, which only sees hopping: its matrix elements are
 `-(i/2) a (n - m) ⟨m|H|n⟩`.
 
 ## Main results
 
-- `toObservable` : a hermitian operator of the chain as an observable on `ℂ^N`.
+- `toObservable` : a hermitian operator of the chain as an observable.
 - `openHamiltonianObservable`, `positionObservable` : `H` and `X` as observables.
 - `inner_bracket_openHamiltonian_position` : the matrix elements of `⁅H, X⁆`.
 - `inner_bracket_openHamiltonian_position_eq` : `⁅H, X⁆` moves exactly one site `a`.
@@ -37,14 +37,12 @@ open ContinuousLinearMap UnitalPositiveLinearMap
 
 namespace CondensedMatter
 namespace TightBindingChain
-open QuantumMechanics.FiniteHilbertSpace
 variable (T : TightBindingChain)
 
-/-- A hermitian operator of the chain as an observable on the site amplitudes in `ℂ^N`. -/
+/-- A hermitian operator of the chain as an observable. -/
 noncomputable def toObservable (A : T.HilbertSpace →ₗ[ℂ] T.HilbertSpace) (hA : A.IsSymmetric) :
-    Observable (EuclideanSpace ℂ (Fin T.N) →L[ℂ] EuclideanSpace ℂ (Fin T.N)) :=
-  ⟨LinearMap.toContinuousLinearMap (isometryEquivEuclidean.toLinearEquiv.conj A),
-    isSelfAdjoint_iff_isSymmetric.mpr fun _ _ => hA _ _⟩
+    Observable (T.HilbertSpace →L[ℂ] T.HilbertSpace) :=
+  ⟨LinearMap.toContinuousLinearMap A, isSelfAdjoint_iff_isSymmetric.mpr hA⟩
 
 /-- The Hamiltonian with open boundary conditions as an observable. -/
 noncomputable abbrev openHamiltonianObservable :=
@@ -55,19 +53,19 @@ noncomputable abbrev positionObservable := T.toObservable T.position T.position_
 
 /-- The bracket `⁅H, X⁆` only connects sites joined by hopping, weighted by their distance. -/
 lemma inner_bracket_openHamiltonian_position (m n : Fin T.N) :
-    ⟪EuclideanSpace.single m (1 : ℂ), ((⁅T.openHamiltonianObservable, T.positionObservable⁆ :
-      Observable _) : _ →L[ℂ] _) (EuclideanSpace.single n (1 : ℂ))⟫_ℂ =
+    ⟪|m⟩, ((⁅T.openHamiltonianObservable, T.positionObservable⁆ : Observable _) :
+      _ →L[ℂ] _) |n⟩⟫_ℂ =
       -(Complex.I / 2) * ((T.a * ((n : ℕ) - (m : ℕ)) : ℝ) : ℂ) *
         ⟪|m⟩, T.openHamiltonian |n⟩⟫_ℂ := by
   rw [selfAdjoint.coe_bracket, smul_apply, inner_smul_right, mul_assoc,
-    ← inner_commutator_position, localizedState, basisFun_apply, basisFun_apply]
+    ← inner_commutator_position]
   rfl
 
 /-- The bracket `⁅H, X⁆` moves the particle exactly one site, a distance `a`, with amplitude
 `± i a t / 2`; every other matrix element vanishes. -/
 lemma inner_bracket_openHamiltonian_position_eq (m n : Fin T.N) :
-    ⟪EuclideanSpace.single m (1 : ℂ), ((⁅T.openHamiltonianObservable, T.positionObservable⁆ :
-      Observable _) : _ →L[ℂ] _) (EuclideanSpace.single n (1 : ℂ))⟫_ℂ =
+    ⟪|m⟩, ((⁅T.openHamiltonianObservable, T.positionObservable⁆ : Observable _) :
+      _ →L[ℂ] _) |n⟩⟫_ℂ =
       if (m : ℕ) + 1 = n then Complex.I * (T.a * T.t / 2 : ℝ)
       else if (n : ℕ) + 1 = m then -(Complex.I * (T.a * T.t / 2 : ℝ)) else 0 := by
   rw [inner_bracket_openHamiltonian_position, inner_openHamiltonian]
@@ -86,7 +84,7 @@ lemma inner_bracket_openHamiltonian_position_eq (m n : Fin T.N) :
 /-- **Energy–position uncertainty of the open tight binding chain.** In every state `ω`,
 `Cov(H, X)² + ⟨⁅H, X⁆⟩² ≤ Var H · Var X`. -/
 lemma robertson_schrodinger_openHamiltonian_position
-    (ω : 𝓢[ℂ, EuclideanSpace ℂ (Fin T.N) →L[ℂ] EuclideanSpace ℂ (Fin T.N)]) :
+    (ω : 𝓢[ℂ, T.HilbertSpace →L[ℂ] T.HilbertSpace]) :
     covariance ω T.openHamiltonianObservable T.positionObservable ^ 2 +
         ω⟨⁅T.openHamiltonianObservable, T.positionObservable⁆⟩ ^ 2 ≤
       variance ω T.openHamiltonianObservable * variance ω T.positionObservable :=