Algebra.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Norm topology on concrete von Neumann algebras

The bicommutant definition used by Mathlib implies norm closedness directly. This supplies the complete C*-algebra structures needed for matrix norms and for the perturbation maps in the manuscript's UCP criterion.

theorem OAI.KadisonKastler.isClosed_algebra line 20
abbrev OAI.KadisonKastler.Algebra line 26
Source documentation
The ordinary complete C*-algebra underlying the concrete algebra.
```
abbrev Algebra (M : VonNeumannAlgebra H) := M.toStarSubalgebra
```
instance OAI.KadisonKastler.algebraCStarAlgebra line 28
theorem OAI.KadisonKastler.isClosed_unitBall line 32
theorem OAI.KadisonKastler.eq_of_kkDistance_eq_zero line 37
Source documentation
Unlike arbitrary nonclosed sets, concrete algebra unit balls are determined by their Hausdorff distance.
```
theorem eq_of_kkDistance_eq_zero {M N : VonNeumannAlgebra H}
    (h : kkDistance M N = 0) : M = N := by
…
```
Mentions: OAI.KadisonKastler.kkDistance