The Jordan–von Neumann reconstruction of a Hermitian form from its quadratic form

Category: 1-Mathlib (CSD-free; staged for upstream). The engine behind both Gleason-type theorems of this repository: Busch's effect version (LF2/EffectGleason.lean, where it was first written) and the projection version (Gleason/ProjectionPackage.lean, Gleason/Descent.lean).

A function q : ℂᴺ → ℝ that scales like q (c • v) = ‖c‖² q v, satisfies the parallelogram law q (u + v) + q (u − v) = 2 q u + 2 q v, and is squeezed between 0 and ‖·‖² is the quadratic form of a unique Hermitian matrix:

• polar q u v = q (u + v) − q (u − v) is bi-additive (IsQuadraticLike.polar_add_left, the Jordan–von Neumann halving identity) and ℝ-bihomogeneous (IsQuadraticLike.polar_smul_real), the upgrade from ℚ to ℝ coming from additive_bounded_linear (Cauchy's equation with a local bound) instead of continuity, which is not assumed;
• sesq q u v = ¼ polar q u v − (i/4) polar q u (i • v) is sesquilinear (IsQuadraticLike.sesq_add_right, sesq_smul_right, sesq_conj_symm) with sesq q v v = q v (IsQuadraticLike.sesq_self);
• polarMatrix q is its matrix on the standard basis: Hermitian (IsQuadraticLike.polarMatrix_isHermitian) with ★ IsQuadraticLike.eq_dotProduct : q v = star v ⬝ᵥ polarMatrix q *ᵥ v.

Also here, the two matrix facts every descent argument needs: a complex matrix is determined by its quadratic form (matrix_eq_zero_of_quadForm_zero) and the trace of a product of Hermitian matrices is real (trace_mul_isHermitian_real), with trace_mul_vecMulVec turning the trace against a rank-one projector into the quadratic form.

Source

Jordan–von Neumann 1935 (the parallelogram characterisation); Busch 2003, quant-ph/9909073 (where the bounded-additive substitute for continuity is used).

Cauchy's functional equation with a local bound

theorem Gleason.additive_bounded_linear (g : ℝ → ℝ) (hadd : ∀ (s t : ℝ), g (s + t) = g s + g t) {M : ℝ} (hM : ∀ (t : ℝ), |t| ≤ 1 → |g t| ≤ M) (x : ℝ) : g x = x * g 1

Cauchy's functional equation with a local bound. An additive g : ℝ → ℝ that is bounded on [-1,1] is linear: g t = t · g 1.

No continuity is assumed. The proof is the classical squeeze on h y = g y − y · g 1: h is additive, kills every integer (h m = m · h 1 = 0), and is bounded on [-1,1]; for any x and any n ≥ 1, n · h x = h (n x − ⌊n x⌋) lands in that bounded window, so |h x| ≤ (M + |g 1|)/n → 0.

Quadratic-like functions

structure Gleason.IsQuadraticLike {N : ℕ} (q : EuclideanSpace ℂ (Fin N) → ℝ) : Prop

A quadratic-like function on ℂᴺ: degree-2 homogeneous under complex scaling, obeying the parallelogram law, and squeezed between 0 and ‖·‖². The last two conditions replace continuity in the Jordan–von Neumann argument (polar_smul_real).

• smul (c : ℂ) (v : EuclideanSpace ℂ (Fin N)) : q (c • v) = ‖c‖ ^ 2 * q v

  q (c • v) = ‖c‖² q v.

• parallelogram (u v : EuclideanSpace ℂ (Fin N)) : q (u + v) + q (u - v) = 2 * q u + 2 * q v

  The parallelogram law.

• nonneg (v : EuclideanSpace ℂ (Fin N)) : 0 ≤ q v

  0 ≤ q.

• le_normSq (v : EuclideanSpace ℂ (Fin N)) : q v ≤ ‖v‖ ^ 2

  q v ≤ ‖v‖².

def Gleason.polar {N : ℕ} (q : EuclideanSpace ℂ (Fin N) → ℝ) (u v : EuclideanSpace ℂ (Fin N)) : ℝ

The polarisation difference polar q u v = q (u + v) − q (u − v) — four times the real part of the sesquilinear form being reconstructed.

Equations

• Gleason.polar q u v = q (u + v) - q (u - v)

noncomputable def Gleason.sesq {N : ℕ} (q : EuclideanSpace ℂ (Fin N) → ℝ) (u v : EuclideanSpace ℂ (Fin N)) : ℂ

The polarised sesquilinear form sesq q u v = ¼ polar q u v − (i/4) polar q u (i • v), the complex polarisation of q.

Equations

• Gleason.sesq q u v = ↑(Gleason.polar q u v) / 4 - Complex.I * ↑(Gleason.polar q u (Complex.I • v)) / 4

noncomputable def Gleason.polarMatrix {N : ℕ} (q : EuclideanSpace ℂ (Fin N) → ℝ) : Matrix (Fin N) (Fin N) ℂ

The matrix of the polarised form on the standard basis, polarMatrix q j k = sesq q eⱼ eₖ.

Equations

• Gleason.polarMatrix q = Matrix.of fun (j k : Fin N) => Gleason.sesq q (EuclideanSpace.single j 1) (EuclideanSpace.single k 1)

theorem Gleason.IsQuadraticLike.zero {N : ℕ} {q : EuclideanSpace ℂ (Fin N) → ℝ} (hq : IsQuadraticLike q) : q 0 = 0

q 0 = 0.

theorem Gleason.IsQuadraticLike.neg {N : ℕ} {q : EuclideanSpace ℂ (Fin N) → ℝ} (hq : IsQuadraticLike q) (v : EuclideanSpace ℂ (Fin N)) : q (-v) = q v

q (−v) = q v.

theorem Gleason.IsQuadraticLike.polar_symm {N : ℕ} {q : EuclideanSpace ℂ (Fin N) → ℝ} (hq : IsQuadraticLike q) (u v : EuclideanSpace ℂ (Fin N)) : polar q u v = polar q v u

polar is symmetric: q (v − u) = q (−(u − v)) = q (u − v).

theorem Gleason.IsQuadraticLike.polar_zero_left {N : ℕ} {q : EuclideanSpace ℂ (Fin N) → ℝ} (hq : IsQuadraticLike q) (v : EuclideanSpace ℂ (Fin N)) : polar q 0 v = 0

polar q 0 v = q v − q (−v) = 0.

theorem Gleason.IsQuadraticLike.polar_neg_right {N : ℕ} {q : EuclideanSpace ℂ (Fin N) → ℝ} (u v : EuclideanSpace ℂ (Fin N)) : polar q u (-v) = -polar q u v

polar q u (−v) = − polar q u v.

theorem Gleason.IsQuadraticLike.polar_add_half {N : ℕ} {q : EuclideanSpace ℂ (Fin N) → ℝ} (hq : IsQuadraticLike q) (u w v : EuclideanSpace ℂ (Fin N)) : polar q u v + polar q w v = 2 * polar q (2⁻¹ • (u + w)) v

The halving identity (Jordan–von Neumann core). polar u v + polar w v = 2 polar ((u+w)/2) v: apply the parallelogram law at (a ± v, b) with a = (u+w)/2, b = (u−w)/2 and subtract the two instances — the q b terms cancel.

theorem Gleason.IsQuadraticLike.polar_add_left {N : ℕ} {q : EuclideanSpace ℂ (Fin N) → ℝ} (hq : IsQuadraticLike q) (u w v : EuclideanSpace ℂ (Fin N)) : polar q (u + w) v = polar q u v + polar q w v

Additivity of polar in the first slot. The halving identity at (u, w) and at (u + w, 0) share a right-hand side.

theorem Gleason.IsQuadraticLike.polar_smul_real {N : ℕ} {q : EuclideanSpace ℂ (Fin N) → ℝ} (hq : IsQuadraticLike q) (t : ℝ) (u v : EuclideanSpace ℂ (Fin N)) : polar q (↑t • u) v = t * polar q u v

Real homogeneity of polar in the first slot. Additivity alone gives ℚ-homogeneity; the upgrade to ℝ is additive_bounded_linear, whose local bound is 0 ≤ q ≤ ‖·‖².

theorem Gleason.IsQuadraticLike.sesq_zero_right {N : ℕ} {q : EuclideanSpace ℂ (Fin N) → ℝ} (u : EuclideanSpace ℂ (Fin N)) : sesq q u 0 = 0

sesq q u 0 = 0.

theorem Gleason.IsQuadraticLike.polar_add_right {N : ℕ} {q : EuclideanSpace ℂ (Fin N) → ℝ} (hq : IsQuadraticLike q) (u v w : EuclideanSpace ℂ (Fin N)) : polar q u (v + w) = polar q u v + polar q u w

Additivity of polar in the second slot (by symmetry).

theorem Gleason.IsQuadraticLike.polar_smul_real_right {N : ℕ} {q : EuclideanSpace ℂ (Fin N) → ℝ} (hq : IsQuadraticLike q) (t : ℝ) (u v : EuclideanSpace ℂ (Fin N)) : polar q u (↑t • v) = t * polar q u v

Real homogeneity of polar in the second slot (by symmetry).

theorem Gleason.IsQuadraticLike.sesq_add_right {N : ℕ} {q : EuclideanSpace ℂ (Fin N) → ℝ} (hq : IsQuadraticLike q) (u v w : EuclideanSpace ℂ (Fin N)) : sesq q u (v + w) = sesq q u v + sesq q u w

Additivity of sesq in the second slot.

theorem Gleason.IsQuadraticLike.sesq_smul_real_right {N : ℕ} {q : EuclideanSpace ℂ (Fin N) → ℝ} (hq : IsQuadraticLike q) (t : ℝ) (u v : EuclideanSpace ℂ (Fin N)) : sesq q u (↑t • v) = ↑t * sesq q u v

Real homogeneity of sesq in the second slot.

theorem Gleason.IsQuadraticLike.sesq_smul_I_right {N : ℕ} {q : EuclideanSpace ℂ (Fin N) → ℝ} (u v : EuclideanSpace ℂ (Fin N)) : sesq q u (Complex.I • v) = Complex.I * sesq q u v

sesq q u (i • v) = i · sesq q u v — pure algebra of the polarisation formula (i·(i·v) = −v), no additivity needed.

theorem Gleason.IsQuadraticLike.sesq_smul_right {N : ℕ} {q : EuclideanSpace ℂ (Fin N) → ℝ} (hq : IsQuadraticLike q) (c : ℂ) (u v : EuclideanSpace ℂ (Fin N)) : sesq q u (c • v) = c * sesq q u v

Complex homogeneity in the second slot: sesq q u (c • v) = c · sesq q u v. Split c = Re c + i · Im c.

theorem Gleason.IsQuadraticLike.sesq_conj_symm {N : ℕ} {q : EuclideanSpace ℂ (Fin N) → ℝ} (hq : IsQuadraticLike q) (u v : EuclideanSpace ℂ (Fin N)) : sesq q v u = (starRingEnd ℂ) (sesq q u v)

Conjugate symmetry: sesq q v u = conj (sesq q u v). The real part is symmetric (polar_symm); the imaginary part flips because q (v ± i·u) = q (u ∓ i·v) (multiply by the unit phase ∓i and use smul). With sesq_smul_right this makes sesq conjugate-linear in its first slot.

theorem Gleason.IsQuadraticLike.sesq_self {N : ℕ} {q : EuclideanSpace ℂ (Fin N) → ℝ} (hq : IsQuadraticLike q) (v : EuclideanSpace ℂ (Fin N)) : sesq q v v = ↑(q v)

sesq restricts to q on the diagonal: sesq q v v = q v. The diagonal value is polar q v v = 4 q v (degree-2 homogeneity at 2), and the imaginary term vanishes: q (v − i·v) = q (v + i·v) (unit phase −i). Both steps are the same witness, IsQuadraticLike.smul (q (c • v) = ‖c‖² q v): at c = 2 it gives the diagonal value, and at c = −i it gives ‖−i‖² = 1, collapsing the imaginary term.

theorem Gleason.IsQuadraticLike.sesq_sum_right {N : ℕ} {q : EuclideanSpace ℂ (Fin N) → ℝ} (hq : IsQuadraticLike q) {ι : Type u_1} (u : EuclideanSpace ℂ (Fin N)) (s : Finset ι) (c : ι → ℂ) (e : ι → EuclideanSpace ℂ (Fin N)) : sesq q u (∑ i ∈ s, c i • e i) = ∑ i ∈ s, c i * sesq q u (e i)

sesq is linear over finite sums in the second slot.

theorem Gleason.IsQuadraticLike.sesq_sum_left {N : ℕ} {q : EuclideanSpace ℂ (Fin N) → ℝ} (hq : IsQuadraticLike q) {ι : Type u_1} (s : Finset ι) (c : ι → ℂ) (e : ι → EuclideanSpace ℂ (Fin N)) (w : EuclideanSpace ℂ (Fin N)) : sesq q (∑ i ∈ s, c i • e i) w = ∑ i ∈ s, (starRingEnd ℂ) (c i) * sesq q (e i) w

sesq is conjugate-linear over finite sums in the first slot.

theorem Gleason.IsQuadraticLike.polarMatrix_isHermitian {N : ℕ} {q : EuclideanSpace ℂ (Fin N) → ℝ} (hq : IsQuadraticLike q) : (polarMatrix q).IsHermitian

polarMatrix q is Hermitian, directly from sesq_conj_symm.

theorem Gleason.euclidean_sum_single {N : ℕ} (v : EuclideanSpace ℂ (Fin N)) : ∑ i : Fin N, v.ofLp i • EuclideanSpace.single i 1 = v

Standard-basis expansion in EuclideanSpace: v = ∑ᵢ vᵢ • eᵢ.

theorem Gleason.IsQuadraticLike.sesq_eq_dotProduct {N : ℕ} {q : EuclideanSpace ℂ (Fin N) → ℝ} (hq : IsQuadraticLike q) (u v : EuclideanSpace ℂ (Fin N)) : sesq q u v = star u.ofLp ⬝ᵥ (polarMatrix q).mulVec v.ofLp

sesq is the sesquilinear form of polarMatrix: sesq q u v = ⟨u, R v⟩. Expand both slots in the standard basis.

theorem Gleason.IsQuadraticLike.eq_dotProduct {N : ℕ} {q : EuclideanSpace ℂ (Fin N) → ℝ} (hq : IsQuadraticLike q) (v : EuclideanSpace ℂ (Fin N)) : ↑(q v) = star v.ofLp ⬝ᵥ (polarMatrix q).mulVec v.ofLp

★ q is the quadratic form of polarMatrix q: q v = ⟨v, R v⟩.

Matrix facts for the descent

theorem Gleason.matrix_eq_zero_of_quadForm_zero {N : ℕ} {D : Matrix (Fin N) (Fin N) ℂ} (hQ : ∀ (x : Fin N → ℂ), star x ⬝ᵥ D.mulVec x = 0) : D = 0

A complex matrix is determined by its quadratic form. If star x ⬝ᵥ (D *ᵥ x) = 0 for every x, then D = 0: over ℂ the diagonal of a sesquilinear form recovers the whole form by polarisation.

theorem Gleason.trace_mul_isHermitian_real {ι : Type u_1} [Fintype ι] {A B : Matrix ι ι ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) : (starRingEnd ℂ) (A * B).trace = (A * B).trace

The trace of a product of two Hermitian matrices is real. conj Tr(A·B) = Tr(B·A) = Tr(A·B).

theorem Gleason.trace_mul_vecMulVec {N : ℕ} (R : Matrix (Fin N) (Fin N) ℂ) (v : EuclideanSpace ℂ (Fin N)) : (R * Matrix.vecMulVec v.ofLp (star v.ofLp)).trace = star v.ofLp ⬝ᵥ R.mulVec v.ofLp

Tr(R · |v⟩⟨v|) = ⟨v, R v⟩. The trace against a rank-one projector is the quadratic form.