KaplanskyGeneral.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The two-by-two step from selfadjoint to arbitrary contractions.

def OAI.KadisonSimilarity.kaplanskyOffDiagonal line 15
Source documentation
The selfadjoint off-diagonal operator associated to a contraction.
```
def kaplanskyOffDiagonal (T : H →L[ℂ] H) : HilbertCopies H 2 →L[ℂ] HilbertCopies H 2 :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies

theorem OAI.KadisonSimilarity.kaplansky_contraction_of_offDiagonal_mem line 20

Source documentation

A matrix-bicommutant membership bridge is the only algebraic fact needed by the two-by-two contraction argument.

theorem kaplansky_contraction_of_offDiagonal_mem
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (T : H →L[ℂ] H) (hT : ‖T‖ ≤ 1)
    (hmem : kaplanskyOffDiagonal T ∈
      representationVonNeumannAlgebra (representedMatrixHom σ 2))
    (s : Finset H) (ε : ℝ) (hε : 0 < ε) :
    ∃ a : A, ‖a‖ ≤ 1 ∧ ∀ x ∈ s, ‖σ a x - T x‖ < ε := by
…

Mentions: OAI.KadisonSimilarity.kaplanskyOffDiagonal, OAI.KadisonSimilarity.representationVonNeumannAlgebra, OAI.KadisonSimilarity.representedMatrixHom