TracialFactorComparison.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Projection comparison in the finite-matrix source follows from its actual normal trace and dense full-matrix tower.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.projectionComparison_of_normal_range line 25
theorem OAI.KadisonSimilarity.matrix_projectionComparison_of_tower line 64
Source documentation
The comparison input for every matrix size in the actual source model.
```
theorem matrix_projectionComparison_of_tower (n : ℕ) [NeZero n] :
    FiniteFactorProjectionComparison
      (fun X : CStarMatrix (Fin n) (Fin n) R => (normalizedMatrixTrace τ n X).re) := by
…
```
Mentions: OAI.KadisonSimilarity.FiniteFactorProjectionComparison, OAI.KadisonSimilarity.normalizedMatrixTrace