KaplanskyDischarge.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Finite-vector Kaplansky density with an exact source norm bound.

theorem OAI.KadisonSimilarity.kaplanskyOffDiagonal_mem line 20
Source documentation
Off-diagonal selfadjoint dilation preserves membership in the matrix bicommutant of the original representation.
```
theorem kaplanskyOffDiagonal_mem (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (T : H →L[ℂ] H) (hT : T ∈ representationVonNeumannAlgebra σ) :
    kaplanskyOffDiagonal T ∈ representationVonNeumannAlgebra (representedMatrixHom σ 2) := by
…
```
Mentions: OAI.KadisonSimilarity.representationVonNeumannAlgebra, OAI.KadisonSimilarity.kaplanskyOffDiagonal, OAI.KadisonSimilarity.representedMatrixHom

theorem OAI.KadisonSimilarity.kaplansky_contraction_approximation line 36

Source documentation

The unit ball of the source algebra is strongly dense in the unit ball of the represented bicommutant, tested on any finite family of vectors.

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

Mentions: OAI.KadisonSimilarity.representationVonNeumannAlgebra

theorem OAI.KadisonSimilarity.kaplansky_finite_approximation line 43

Source documentation

Scaling the unit-ball statement retains the exact norm of the target.

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

Mentions: OAI.KadisonSimilarity.representationVonNeumannAlgebra

theorem OAI.KadisonSimilarity.twoVectorKaplanskyInput line 85
Source documentation
Two-vector Kaplansky approximation, using the canonical spectral order on the matrix C-star algebra.
```
theorem twoVectorKaplanskyInput (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) :
    TwoVectorKaplanskyInput σ (representationVonNeumannAlgebra σ) := by
…
```
Mentions: OAI.KadisonSimilarity.TwoVectorKaplanskyInput, OAI.KadisonSimilarity.representationVonNeumannAlgebra