Wigner's theorem over the reals

The statement

A map from the rays of a finite-dimensional real inner-product space to themselves preserves every transition probability. Then it is induced by a linear isometry equivalence of the space. Bijectivity of the ray map isn’t assumed; it follows from the conclusion.

For nonzero representatives ψ and φ, the transition probability is

P(ψ, φ) = |⟨ψ, φ⟩|² / (‖ψ‖² ‖φ‖²).

A ray is a one-dimensional subspace, so rescaling its representative doesn’t change this value.

Hypotheses

• The carrier E is a nontrivial, finite-dimensional real inner-product space.
• f is an arbitrary self-map of its projective space, ℙ ℝ E.
• For every pair of rays, f preserves the transition probability exactly. No continuity or bijectivity hypothesis is added.

What’s not proved

This entry is the real, finite-dimensional theorem. It doesn’t state the complex unitary-or-antiunitary case, an infinite-dimensional theorem, or a stability estimate for approximate preservation.

It also isn’t the Uhlhorn theorem: preserving only orthogonality is a different hypothesis from preserving all transition probabilities.

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]

theorem exists_isometry_of_transProbPreserving [FiniteDimensional ℝ E] [Nontrivial E]
    {f : ℙ ℝ E → ℙ ℝ E} (hf : TransProbPreserving f) :
    ∃ e : E ≃ₗᵢ[ℝ] E, ∀ p : ℙ ℝ E, f p = projMap e p