OAI/Analysis/KadisonSimilarity/Tracial/TracialMatrixDiffuse.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Arbitrarily small full-matrix corners and comparison split every nonzero projection in the source algebra.

  1. theorem OAI.KadisonSimilarity.TracialCornerGeometry.proper_subprojection_of_matrix_tower line 21

    Source documentation

    A nonzero projection contains a proper nonzero subprojection.

    theorem proper_subprojection_of_matrix_tower
    (hf : Function.Injective G.vector)
    (comparison : FiniteFactorProjectionComparison (fun a => (G.trace a).re))
    (hsize : Filter.Tendsto (fun j => (Fintype.card (I j) : ℝ)) Filter.atTop Filter.atTop)
    (p : P) (hp : IsStarProjection p) (hp0 : p ≠ 0) :
    ∃ q : P, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p * q = q ∧ q * p = q := by
…

    Mentions: OAI.KadisonSimilarity.FiniteFactorProjectionComparison