Projector Range Orthonormal Bases

This file packages the finite-dimensional spectral decomposition of an orthogonal projector as an orthonormal basis of its range. It supplies the rank-one decomposition needed by the rank-reduction truncation branch in the low-degree-test formalization.

References

• references/ldt-paper/orthonormalization.tex, lines 570--573.
• MIPStarRE/LDT/MakingMeasurementsProjective/QXPLayer/RankReduction/LowRank.lean.

theorem MIPStarRE.Quantum.hermitian_eq_sum_eigenvalues_vecMulVec {ι : Type u_1} [Fintype ι] [DecidableEq ι] (A : Op ι) (hA : Matrix.IsHermitian A) : A = ∑ i : ι, ↑(hA.eigenvalues i) • Matrix.vecMulVec (hA.eigenvectorBasis i).ofLp (star (hA.eigenvectorBasis i).ofLp)

Spectral expansion of a Hermitian matrix as a sum of rank-one eigenvector projectors weighted by eigenvalues.

theorem MIPStarRE.Quantum.IsProj.eigenvalues_zero_or_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (P : Op ι) (hP : IsProj P) (i : ι) : ⋯.eigenvalues i = 0 ∨ ⋯.eigenvalues i = 1

For a Hermitian idempotent matrix, every eigenvalue is either 0 or 1.

theorem MIPStarRE.Quantum.IsProj.eq_sum_nonzero_eigenvector_projectors {ι : Type u_1} [Fintype ι] [DecidableEq ι] (P : Op ι) (hP : IsProj P) : P = ∑ i : { i : ι // ⋯.eigenvalues i ≠ 0 }, Matrix.vecMulVec (⋯.eigenvectorBasis ↑i).ofLp (star (⋯.eigenvectorBasis ↑i).ofLp)

A projector is the sum of the rank-one projectors onto the eigenvectors with nonzero eigenvalue. For a projector these are exactly the 1-eigenvectors.

theorem MIPStarRE.Quantum.IsProj.trace_eq_rank {ι : Type u_1} [Fintype ι] (Q : Op ι) (hQ : IsProj Q) : Matrix.trace Q = ↑(Matrix.rank Q)

The trace of a finite-dimensional orthogonal projector equals its rank.

structure MIPStarRE.Quantum.ProjectorRangeONB {ι : Type u_1} [Fintype ι] (P : Op ι) (hP : IsProj P) : Type u_1

A rank-indexed orthonormal basis of the range of a projector, packaged with the corresponding rank-one decomposition.

• vec : Fin (Matrix.rank P) → ι → ℂ

  The chosen range basis vectors.

• orthonormal (i j : Fin (Matrix.rank P)) : star (self.vec i) ⬝ᵥ self.vec j = if i = j then 1 else 0

  The chosen vectors are orthonormal.

• decomposition : P = ∑ i : Fin (Matrix.rank P), Matrix.vecMulVec (self.vec i) (star (self.vec i))

  The projector decomposes as the sum of the rank-one projectors onto the chosen range basis.

noncomputable def MIPStarRE.Quantum.ProjectorRangeONB.rankOne {ι : Type u_1} [Fintype ι] {P : Op ι} {hP : IsProj P} (b : ProjectorRangeONB P hP) (i : Fin (Matrix.rank P)) : Op ι

The rank-one projector attached to one vector of a projector range ONB.

Equations

• b.rankOne i = Matrix.vecMulVec (b.vec i) (star (b.vec i))

noncomputable def MIPStarRE.Quantum.ProjectorRangeONB.subprojector {ι : Type u_1} [Fintype ι] {P : Op ι} {hP : IsProj P} (b : ProjectorRangeONB P hP) (S : Finset (Fin (Matrix.rank P))) : Op ι

The partial projector obtained by summing a subset of range ONB rank-one projectors.

Equations

• b.subprojector S = ∑ i ∈ S, b.rankOne i

@[simp]

theorem MIPStarRE.Quantum.ProjectorRangeONB.rankOne_apply {ι : Type u_1} [Fintype ι] {P : Op ι} {hP : IsProj P} (b : ProjectorRangeONB P hP) (i : Fin (Matrix.rank P)) : b.rankOne i = Matrix.vecMulVec (b.vec i) (star (b.vec i))

theorem MIPStarRE.Quantum.ProjectorRangeONB.rankOne_mul {ι : Type u_1} [Fintype ι] {P : Op ι} {hP : IsProj P} (b : ProjectorRangeONB P hP) (i j : Fin (Matrix.rank P)) : b.rankOne i * b.rankOne j = if i = j then b.rankOne i else 0

Rank-one projectors from an orthonormal family multiply as Kronecker deltas.

theorem MIPStarRE.Quantum.ProjectorRangeONB.rankOne_mulVec_vec {ι : Type u_1} [Fintype ι] {P : Op ι} {hP : IsProj P} (b : ProjectorRangeONB P hP) (i j : Fin (Matrix.rank P)) : Matrix.mulVec (b.rankOne i) (b.vec j) = if i = j then b.vec i else 0

A rank-one projector from the chosen range basis acts by the corresponding Kronecker delta on basis vectors.

theorem MIPStarRE.Quantum.ProjectorRangeONB.mulVec_vec {ι : Type u_1} [Fintype ι] {P : Op ι} {hP : IsProj P} (b : ProjectorRangeONB P hP) (i : Fin (Matrix.rank P)) : Matrix.mulVec P (b.vec i) = b.vec i

Each vector in the chosen orthonormal basis of the range is fixed by the projector.

theorem MIPStarRE.Quantum.ProjectorRangeONB.subprojector_isHermitian {ι : Type u_1} [Fintype ι] {P : Op ι} {hP : IsProj P} (b : ProjectorRangeONB P hP) (S : Finset (Fin (Matrix.rank P))) : Matrix.IsHermitian (b.subprojector S)

A selected sum of orthonormal rank-one projectors is Hermitian.

theorem MIPStarRE.Quantum.ProjectorRangeONB.subprojector_idempotent {ι : Type u_1} [Fintype ι] {P : Op ι} {hP : IsProj P} (b : ProjectorRangeONB P hP) (S : Finset (Fin (Matrix.rank P))) : b.subprojector S * b.subprojector S = b.subprojector S

A selected sum of orthonormal rank-one projectors is idempotent.

theorem MIPStarRE.Quantum.ProjectorRangeONB.subprojector_isProj {ι : Type u_1} [Fintype ι] {P : Op ι} {hP : IsProj P} (b : ProjectorRangeONB P hP) (S : Finset (Fin (Matrix.rank P))) : IsProj (b.subprojector S)

A selected sum of orthonormal rank-one projectors is a projector.

theorem MIPStarRE.Quantum.ProjectorRangeONB.subprojector_trace {ι : Type u_1} [Fintype ι] {P : Op ι} {hP : IsProj P} (b : ProjectorRangeONB P hP) (S : Finset (Fin (Matrix.rank P))) : Matrix.trace (b.subprojector S) = ↑S.card

The partial projector's trace is the number of selected vectors.

theorem MIPStarRE.Quantum.ProjectorRangeONB.subprojector_rank {ι : Type u_1} [Fintype ι] {P : Op ι} {hP : IsProj P} (b : ProjectorRangeONB P hP) (S : Finset (Fin (Matrix.rank P))) : Matrix.rank (b.subprojector S) = S.card

The rank of a selected sum is exactly the number of selected ONB vectors.

theorem MIPStarRE.Quantum.ProjectorRangeONB.subprojector_add_compl {ι : Type u_1} [Fintype ι] {P : Op ι} {hP : IsProj P} (b : ProjectorRangeONB P hP) (S : Finset (Fin (Matrix.rank P))) : b.subprojector S + b.subprojector Sᶜ = P

A partial projector plus its complementary partial projector is the original projector.

theorem MIPStarRE.Quantum.ProjectorRangeONB.subprojector_diff_eq_compl {ι : Type u_1} [Fintype ι] {P : Op ι} {hP : IsProj P} (b : ProjectorRangeONB P hP) (S : Finset (Fin (Matrix.rank P))) : P - b.subprojector S = b.subprojector Sᶜ

The difference between a projector and a partial projector is the complementary partial projector.

theorem MIPStarRE.Quantum.ProjectorRangeONB.subprojector_le {ι : Type u_1} [Fintype ι] {P : Op ι} {hP : IsProj P} (b : ProjectorRangeONB P hP) (S : Finset (Fin (Matrix.rank P))) : b.subprojector S ≤ P

A partial projector is dominated by the original projector.

noncomputable def MIPStarRE.Quantum.IsProj.rangeONB {ι : Type u_1} [Fintype ι] [DecidableEq ι] (P : Op ι) (hP : IsProj P) : ProjectorRangeONB P hP

Choose an orthonormal basis of the range of a projector using Mathlib's Hermitian spectral theorem.

Equations

• One or more equations did not get rendered due to their size.