OAI/Analysis/KadisonSimilarity/Tracial/SmallTraceFrames.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An unbounded matrix tower supplies the small corner and its complete finite partial-isometry frame used in the free-corner argument.

  1. theorem OAI.KadisonSimilarity.NestedTracialMatrices.exists_small_trace_frame line 21

    Source documentation

    The corner may be chosen below any positive prescribed trace bound. Its matrix-unit column resolves the identity, so no frame existence is an additional hypothesis.

    theorem NestedTracialMatrices.exists_small_trace_frame
    (M : NestedTracialMatrices (A := I) τ V)
…

    Mentions: OAI.KadisonSimilarity.NestedTracialMatrices