  16  self_adjoint : ∀ x y : H, ⟪op x, y⟫_ℂ = ⟪x, op y⟫_ℂ
  17
  18/-- Projection operator -/
  19structure Projector (H : Type*) [RSHilbertSpace H] extends Observable H where
  20  /-- Idempotent property -/
  21  idempotent : op.comp op = op
  22
  23/-- Hamiltonian operator -/
  24structure Hamiltonian (H : Type*) [RSHilbertSpace H] extends Observable H where
  25  /-- Energy must be bounded below -/
  26  bounded_below : ∃ E₀ : ℝ, ∀ ψ : NormalizedState H,
  27    (⟪op ψ.vec, ψ.vec⟫_ℂ).re ≥ E₀
  28
  29end IndisputableMonolith.Quantum

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.