AdaptedMatrixRefinement.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.KadisonKastler.adaptedMatrixUnits_retains line 22
Source documentation
Rank-one units for the adapted basis retain each old matrix entry as a sum over the new index.
```
theorem adaptedMatrixUnits_retains (i j : ι) :
    ∑ r, (Generator.orthonormalMatrixUnits (E.adaptedBasis o b)).entry (i, r) (j, r) =
      E.entry i j := by
…
```
Mentions: OAI.Generator.orthonormalMatrixUnits
theorem OAI.KadisonKastler.adaptedMatrixUnits_group_le line 43
Source documentation
This full matrix refinement contains the old finite signed group.
```
theorem adaptedMatrixUnits_group_le :
    matrixSignedGroup E ≤ matrixSignedGroup (Generator.orthonormalMatrixUnits (E.adaptedBasis o b)) :=
…
```
Mentions: OAI.KadisonKastler.matrixSignedGroup, OAI.Generator.orthonormalMatrixUnits
theorem OAI.KadisonKastler.exists_fullMatrix_refinement line 49
Source documentation
The refined matrix system generates every operator on the finite Hilbert space and keeps the previous signed group.
```
theorem exists_fullMatrix_refinement [FiniteDimensional ℂ H] (o : ι) :
    ∃ (r : ℕ) (F : Generator.MatrixUnitSystem (ι × Fin r) (H →L[ℂ] H)),
      Function.Surjective F.hom ∧ matrixSignedGroup E ≤ matrixSignedGroup F := by
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.matrixSignedGroup