OAI/Analysis/KadisonKastler/NormalizedMatrixAveraging.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Faithful central unit vectors from finite matrix averaging

The explicit central-vector projection of a faithful positive unit vector is nonzero. Normalizing it retains positivity, faithfulness and cyclicity, with at most twice the displacement of the orthogonal projection.

  1. theorem OAI.KadisonKastler.exists_positive_matrix_central_unit_vector line 25