Lemma 3.6

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.orthogonal_representation_independence

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $\mathcal A$ be an abelian von Neumann algebra. If $A$ has two finite orthogonal representations $A=\sum_j b_jP_j=\sum_k c_kQ_k$ by nonzero projections, then the complex-valued functions on $Q(\mathcal A)$ agree:

\sum_j b_j\chi_{Q_{P_j}(\mathcal A)} =\sum_k c_k\chi_{Q_{Q_k}(\mathcal A)}.

Zero coefficients are allowed. The equality is of functions, not evaluation at the operator $A$ .

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P20

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P20

open Set TopologicalSpace

open QAlgorithms.Papers.Independent.Next46.P33 (Projection)

open scoped Topology

universe u v

/-- Lemma 3.6; de Groote, Observables I, PDF p./pp. 60.
-/
theorem orthogonal_representation_independence {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (R : VonNeumannAlgebra H)
    (hcomm : ∀ a b : R.toStarSubalgebra, a * b = b * a) (x : R.toStarSubalgebra)
    {m n : ℕ} (b : Fin m → ℂ) (p : Fin m → Projection R)
    (c : Fin n → ℂ) (q : Fin n → Projection R)
    (hp : IsOrthogonalRepresentation x b p) (hq : IsOrthogonalRepresentation x c q) :
    spectralSumFunction b p = spectralSumFunction c q := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 60, Lemma 3.6

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $H$ be a complete complex inner product space, and let $R$ be a von Neumann algebra of bounded complex-linear operators on $H$ , with $ab=ba$ for every $a,b\in R$ . Fix $x\in R$ , arbitrary natural numbers $m,n$ , complex coefficients $b_i$ for $0\leq i<m$ and $c_j$ for $0\leq j<n$ , and projections $p_i,q_j\in R$ , where a projection is a self-adjoint idempotent operator. Suppose every $p_i$ and every $q_j$ is nonzero, $p_ip_k=0$ for distinct indices $i,k$ , $q_jq_\ell=0$ for distinct indices $j,\ell$ , and

x=\sum_{i=0}^{m-1}b_i p_i=\sum_{j=0}^{n-1}c_j q_j.

Then, for every quasipoint $B$ of the projections of $R$ ,

\sum_{\substack{0\leq i<m\\p_i\in B}}b_i = \sum_{\substack{0\leq j<n\\q_j\in B}}c_j.

Here $B$ is a nonempty family of projections excluding zero, every pair has a common lower bound in $B$ in the inherited operator order, and $B$ is maximal under inclusion among families with these properties. The coefficients need not be nonzero. Either index set may be empty: its nonzero and orthogonality conditions are then vacuous, its operator sum is zero, and its scalar sum is zero.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph