FiniteDimensionalGap.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite dimensionality across a small algebra gap

A finite net in the second unit ball produces a net of radius less than one in the first unit ball. Riesz's lemma then forces finite dimensionality. Only the fixed small constant needed in the type-stability argument is used.

theorem OAI.KadisonKastler.finiteDimensional_of_unitBall_approx line 19
theorem OAI.KadisonKastler.finiteDimensional_of_near_finiteDimensional line 73
Source documentation
A neighbor of a finite-dimensional algebra at the constant used in the finite-type theorem is itself finite-dimensional.
```
theorem finiteDimensional_of_near_finiteDimensional
    (M N : VonNeumannAlgebra H) [FiniteDimensional ℂ (Algebra N)]
    (hgap : kkDistance M N < 1 / 10) : FiniteDimensional ℂ (Algebra M) := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.kkDistance