quantum_unitary_preserves_inner

theoremverified

For any unitary continuous linear operator U on a complex Hilbert space E and any vectors ϕ and ψ in E, the inner product is preserved: ⟪U ϕ, U ψ⟫_ℂ = ⟪ϕ, ψ⟫_ℂ.

Statement

theorem quantum_unitary_preserves_inner {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]
    (U : E →L[ℂ] E) (hU : U ∈ unitary (E →L[ℂ] E)) (ϕ ψ : E) :
    inner ℂ (U ϕ) (U ψ) = inner ℂ ϕ ψ

Source: Hall, Quantum Theory for Mathematicians, Definition 2.14; von Neumann, Mathematical Foundations of Quantum Mechanics, ch. II.8
Verified: 11 Sep 2026
Axioms: Classical.choiceQuot.soundpropext

Read back from the Lean

Let $E$ be a complete complex inner product space (a Hilbert space). For every continuous $\mathbb{C}$-linear operator $U : E \to L[\mathbb{C}] E$ that is unitary (i.e., an element of unitary (E →L[ℂ] E)), and for all vectors $\phi, \psi \in E$, the complex inner product $\langle U(\phi), U(\psi) \rangle_{\mathbb{C}}$ equals $\langle \phi, \psi \rangle_{\mathbb{C}}$.

Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.

Lean source view module on GitHub

/-- A unitary operator preserves the complex inner product between states. -/
theorem quantum_unitary_preserves_inner {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]
    (U : E →L[ℂ] E) (hU : U ∈ unitary (E →L[ℂ] E)) (ϕ ψ : E) :
    inner ℂ (U ϕ) (U ψ) = inner ℂ ϕ ψ := by
  rw [← ContinuousLinearMap.adjoint_inner_right]
  change inner ℂ ϕ ((star U * U) ψ) = inner ℂ ϕ ψ
  rw [hU.1]
  rfl

Discuss this result Challenge it