TypeIIISpectralMatrix.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Finite spectral partitions in a type III factor are matrix diagonals

theorem OAI.KadisonKastler.TypeIIIFactor.exists_matrixUnits_of_partition line 23

Source documentation

Nonzero orthogonal spectral pieces summing to one are the diagonal of an actual full matrix system in the original type III factor.

theorem TypeIIIFactor.exists_matrixUnits_of_partition (hM : TypeIIIFactor M)
    (q : ι → AlgebraProjection M) (hne : ∀ i, (q i).val ≠ 0)
    (horth : ∀ i j, i ≠ j → (q i).val * (q j).val = 0)
    (htotal : ∑ i, (q i).val = 1) :
    ∃ E : MatrixUnitSystem ι (Algebra M), ∀ i, E.entry i i = (q i).val := by
…

Mentions: OAI.KadisonKastler.TypeIIIFactor, OAI.KadisonKastler.Algebra

abbrev OAI.KadisonKastler.spectralPartitionNonzeroIndex line 58
Source documentation
Discard the zero spectral pieces without changing the spectral sum.
```
abbrev spectralPartitionNonzeroIndex {p : AlgebraProjection M} (Q : CornerPartition p) :=
…
```
instance OAI.KadisonKastler.spectralPartitionNonzeroIndexFintype line 61
instance OAI.KadisonKastler.spectralPartitionNonzeroIndexDecidableEq line 66
theorem OAI.KadisonKastler.spectralPartitionSum_nonzero line 70
theorem OAI.KadisonKastler.spectralPartition_nonempty_nonzeroIndex line 87
Source documentation
A nonzero partition of the identity has a nonzero piece.
```
theorem spectralPartition_nonempty_nonzeroIndex [Nontrivial H] (Q : CornerPartition (identityProjection M)) :
    Nonempty (spectralPartitionNonzeroIndex Q) := by
…
```
Mentions: OAI.KadisonKastler.spectralPartitionNonzeroIndex
theorem OAI.KadisonKastler.TypeIIIFactor.exists_spectral_matrixUnits line 101
Source documentation
Every finite spectral partition in the type III factor is contained in one finite full matrix algebra, after dropping its zero pieces.
```
theorem TypeIIIFactor.exists_spectral_matrixUnits (hM : TypeIIIFactor M)
    (Q : CornerPartition (identityProjection M)) :
    ∃ E : MatrixUnitSystem (spectralPartitionNonzeroIndex Q) (Algebra M),
      ∀ i, E.entry i i = (Q.piece i.val).val := by
…
```
Mentions: OAI.KadisonKastler.TypeIIIFactor, OAI.KadisonKastler.spectralPartitionNonzeroIndex, OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.TypeIIIFactor.exists_selfAdjoint_matrix_approx line 116

Source documentation

A self-adjoint element of a type III factor is approximated in norm by an element of a finite full matrix algebra in the same representation.

theorem TypeIIIFactor.exists_selfAdjoint_matrix_approx [Nontrivial H]
    (hM : TypeIIIFactor M) (x : Algebra M) (hx : IsSelfAdjoint x)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ (n : ℕ) (E : MatrixUnitSystem (Fin n) (H →L[ℂ] H)), 0 < n ∧
      E.algebra ≤ M.toStarSubalgebra ∧
      ∃ y ∈ E.algebra, ‖x.val - y‖ < ε := by
…

Mentions: OAI.KadisonKastler.TypeIIIFactor, OAI.KadisonKastler.Algebra