OAI/Analysis/Quasitrace/Infiniteness.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Proper infiniteness, isometry columns, and C-star matrix amplification.

  1. def OAI.Kaplansky.ProperlyInfinite line 18

    Also declared: ComparatorChallenges/KaplanskyStableFiniteness.lean:122 (same declaration text).

  2. theorem OAI.Kaplansky.not_properlyInfinite line 21
  3. def OAI.Kaplansky.properIsometryColumns line 72
  4. theorem OAI.Kaplansky.properIsometryColumns_column line 80

    Source documentation

    The rectangular concatenation of a pair of orthogonal isometries has column adjoint-square identity, with exactly 2m input columns.

    theorem properIsometryColumns_column (s t : CStarMatrix (Fin m) (Fin m) A)
    (hs : star s*s=1) (ht : star t*t=1) (hst : star s*t=0) (i j : Fin (m+m)) :
    (∑ row, star (properIsometryColumns s t row i)*properIsometryColumns s t row j) =
      if i=j then (1 : A) else 0 := by
…

    Mentions: OAI.Kaplansky.properIsometryColumns

  5. theorem OAI.Kaplansky.properlyInfinite_map line 105
  6. theorem OAI.Kaplansky.properlyInfinite_starAlgEquiv_iff line 113
  7. def OAI.Kaplansky.cstarMatrixFlatten line 121

    Source documentation

    Flatten the two genuine C*-matrix levels into one product-indexed matrix algebra, preserving multiplication, star, and complex scalars.

    def cstarMatrixFlatten : CStarMatrix m m (CStarMatrix n n A) ≃⋆ₐ[ℂ]
    CStarMatrix (m × n) (m × n) A where
…