quantum_projection_expectation_norm_sq

theoremverified

For any orthogonal projection operator P (a self-adjoint idempotent continuous linear map) on a complex Hilbert space E and any state vector ψ in E, the inner product ⟪ψ, P ψ⟫_ℂ equals the complex square of the norm ‖P ψ‖.

Statement

theorem quantum_projection_expectation_norm_sq {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]
    (P : E →L[ℂ] E) (hP : IsStarProjection P) (ψ : E) :
    inner ℂ ψ (P ψ) = (‖P ψ‖ : ℂ) ^ 2

Source: von Neumann, Mathematical Foundations of Quantum Mechanics, ch. III.1; Nielsen & Chuang, Quantum Computation and Quantum Information, sec. 2.2.5
Verified: 11 Sep 2026
Axioms: Classical.choiceQuot.soundpropext

Read back from the Lean

Let $E$ be a type equipped with the structures of a normed additive commutative group, an inner product space over the complex numbers $\mathbb{C}$, and a complete space (i.e., a complex Hilbert space). Let $P : E \toL[\mathbb{C}] E$ be a continuous $\mathbb{C}$-linear map on $E$, assume that $P$ is a star-projection (IsStarProjection P, meaning $P$ is self-adjoint, $\operatorname{star} P = P$, and idempotent, $P^2 = P$), and let $\psi \in E$. Then the complex inner product of $\psi$ and $P(\psi)$ equals the square of the norm of $P(\psi)$ coerced to $\mathbb{C}$, that is, $\langle \psi, P(\psi) \rangle_{\mathbb{C}} = (\|P(\psi)\| : \mathbb{C})^2$.

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

/-- The expectation value of an orthogonal projection operator equals the squared norm of the projected state. -/
theorem quantum_projection_expectation_norm_sq {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]
    (P : E →L[ℂ] E) (hP : IsStarProjection P) (ψ : E) :
    inner ℂ ψ (P ψ) = (‖P ψ‖ : ℂ) ^ 2 := by
  have h_adj : ContinuousLinearMap.adjoint P = P :=
    (ContinuousLinearMap.star_eq_adjoint P).symm.trans hP.isSelfAdjoint.star_eq
  have h_idem : P (P ψ) = P ψ := congr_arg (· ψ) hP.isIdempotentElem
  nth_rw 1 [← h_idem]
  rw [← ContinuousLinearMap.adjoint_inner_left, h_adj]
  exact inner_self_eq_norm_sq_to_K (P ψ)

Discuss this result Challenge it