Transition probability on complex projective space

Category: 1-Mathlib (CSD-free Mathlib upstream candidate).

For two rays p, q in the complex projective space ℙ ℂ E of a complex inner-product space E, the transition probability is the phase-invariant quadratic form

transProb p q = ‖⟪p.rep, q.rep⟫‖² / (‖p.rep‖² · ‖q.rep‖²),

the squared overlap of the two rays normalised to representative norms. On normalised representatives this is the Born weight ‖⟪ψ, φ⟫‖²; the normalisation makes it independent of the chosen representatives, hence a genuine function of the projective points.

This file delivers the transition-probability API plus the forward (realisability) direction of the Wigner / Fubini–Study rigidity correspondence:

• transProbVec — the vector-level form, with scaling invariance in each argument (transProbVec_smul_left/right), the bounds transProbVec_nonneg, transProbVec_le_one, and the diagonal normalisation transProbVec_self.
• transProb — the projective form, with the load-bearing well-definedness rewriter transProb_mk valid for arbitrary nonzero representatives.
• transProb_smul_unitary — the forward direction: every unitary in Matrix.unitaryGroup (Fin N) ℂ, acting on ℂℙ^{N-1}, preserves the transition probability. This is the U(N) ⊆ transition-preservers half of the rigidity correspondence.
• transProb_eq_one_iff / transProb_eq_zero_iff — the equality and orthogonality characterisations (coincidence and orthogonality of rays), the provable hooks for the converse.

Open target (not proved here): the Wigner / Fubini–Study converse

The converse of transProb_smul_unitary is the Wigner / Fubini–Study rigidity theorem: every transition-probability-preserving self-map of ℙ ℂ E is induced by a unitary (equivalently, the isometry group of ℂℙⁿ with the Fubini–Study metric is the projective unitary group PU(n+1)). This is multi-session Mathlib-gap mathematics — it requires phase-coherence bookkeeping, extraction of (semi)linearity from the overlap data, and ruling out the antiunitary branch via the Kähler complex structure (over ℂ, transition-probability preservation alone admits both the unitary and antiunitary classes; the holomorphic / Kähler structure selects the unitary one). It is not stated here as an axiom or a sorry; this file is the foundation on which it will eventually be stated.

Provenance

Staged as upstream Mathlib material. All declarations live under namespace Projectivization with no CsdLean4-namespace prefix; the CsdLean4/Mathlib/... location is the only staging signal. Intended location: Mathlib/LinearAlgebra/Projectivization/TransitionProbability.lean.

Tags

projectivization, transition probability, Fubini-Study, Wigner theorem, unitary group, complex projective space

Vector-level transition probability

noncomputable def Projectivization.transProbVec {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ φ : E) : ℝ

The vector-level transition probability of two vectors ψ, φ in a complex inner-product space: the squared overlap normalised by the squared norms. On unit vectors this is the Born weight ‖⟪ψ, φ⟫‖². The inner-product orientation is Mathlib's: inner ℂ ψ φ is conjugate-linear in ψ and linear in φ; the form is insensitive to this choice.

Equations

• Projectivization.transProbVec ψ φ = ‖inner ℂ ψ φ‖ ^ 2 / (‖ψ‖ ^ 2 * ‖φ‖ ^ 2)

theorem Projectivization.transProbVec_smul_left {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {c : ℂ} (hc : c ≠ 0) (ψ φ : E) : transProbVec (c • ψ) φ = transProbVec ψ φ

Scaling the first argument by a nonzero scalar leaves transProbVec unchanged: the ‖c‖² introduced in the numerator (via inner_smul_left, the conjugate factor having equal norm) cancels the one in the denominator.

theorem Projectivization.transProbVec_smul_right {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {c : ℂ} (hc : c ≠ 0) (ψ φ : E) : transProbVec ψ (c • φ) = transProbVec ψ φ

Scaling the second argument by a nonzero scalar leaves transProbVec unchanged.

theorem Projectivization.transProbVec_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ φ : E) : 0 ≤ transProbVec ψ φ

transProbVec is nonnegative.

theorem Projectivization.transProbVec_le_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ φ : E) : transProbVec ψ φ ≤ 1

transProbVec is bounded by 1, by Cauchy–Schwarz (norm_inner_le_norm). The degenerate cases ψ = 0 or φ = 0 make the denominator zero, so the quotient is 0 ≤ 1 by the div_zero convention.

theorem Projectivization.transProbVec_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ψ : E} (h : ψ ≠ 0) : transProbVec ψ ψ = 1

The diagonal value is 1 for any nonzero vector: ⟪ψ, ψ⟫ = ‖ψ‖².

Projective transition probability

noncomputable def Projectivization.transProb {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (p q : Projectivization ℂ E) : ℝ

The transition probability between two projective points, defined on their canonical (nonzero) representatives Projectivization.rep. The well-definedness across the choice of representative is transProb_mk.

Equations

• p.transProb q = Projectivization.transProbVec p.rep q.rep

theorem Projectivization.rep_mk_eq_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {v : E} (hv : v ≠ 0) : ∃ (a : ℂˣ), (mk ℂ v hv).rep = a • v

A canonical representative of mk v hv is a nonzero scalar multiple of v.

theorem Projectivization.transProb_mk {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {v w : E} (hv : v ≠ 0) (hw : w ≠ 0) : (mk ℂ v hv).transProb (mk ℂ w hw) = transProbVec v w

Well-definedness rewriter. For arbitrary nonzero representatives v, w, the projective transition probability equals the vector-level form on v, w. The canonical reps differ from v, w by nonzero scalars, which the scaling-invariance lemmas absorb.

Forward (realisability) direction: U(N) ⊆ transition-preservers

theorem Projectivization.inner_toEuclideanLin_unitary {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (v w : EuclideanSpace ℂ (Fin N)) : inner ℂ ((Matrix.toEuclideanLin ↑U) v) ((Matrix.toEuclideanLin ↑U) w) = inner ℂ v w

Unitary inner-product preservation on EuclideanSpace ℂ (Fin N): ⟪U v, U w⟫ = ⟪v, w⟫ for U a matrix-unitary, where the action is the toEuclideanLin of the matrix. Routes through EuclideanSpace.inner_eq_star_dotProduct, star_mulVec, and the unitary relation Uᴴ * U = 1.

theorem Projectivization.smul_mk_eq_mk_toEuclideanLin {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) {v : EuclideanSpace ℂ (Fin N)} (hv : v ≠ 0) : U • mk ℂ v hv = mk ℂ ((Matrix.toEuclideanLin ↑U) v) ⋯

The unitary action sends mk v to mk (toEuclideanLin U v).

theorem Projectivization.transProb_smul_unitary {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p q : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : (U • p).transProb (U • q) = p.transProb q

Forward (realisability) direction. Every unitary in Matrix.unitaryGroup (Fin N) ℂ, acting on ℂℙ^{N-1}, preserves the transition probability:

transProb (U • p) (U • q) = transProb p q.

This is the U(N) ⊆ transition-preservers half of the Wigner / Fubini–Study rigidity correspondence. The converse (a transition-preserving self-map is induced by a unitary) is the open target documented in the module header.

Equality and orthogonality characterisations (converse hooks)

theorem Projectivization.transProb_eq_one_iff {N : ℕ} (p q : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : p.transProb q = 1 ↔ p = q

Coincidence characterisation. The transition probability is 1 iff the two projective points are equal. The forward implication is the Cauchy–Schwarz equality case (norm_inner_eq_norm_iff): saturation forces the representatives to be parallel, hence the same projective point.

theorem Projectivization.transProb_eq_zero_iff {N : ℕ} (p q : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : p.transProb q = 0 ↔ inner ℂ p.rep q.rep = 0

Orthogonality characterisation. The transition probability is 0 iff the representatives are orthogonal. Since both representatives are nonzero, the denominator is nonzero, so the quotient vanishes iff the numerator does, i.e. iff ‖⟪p.rep, q.rep⟫‖ = 0.