Main.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The uniformly bounded nonunitarizable representation of a countable nonamenable group, assembled from sparse masks, frames, and the direct-sum obstruction.

theorem OAI.Dixmier.nonamenable_witness line 18
Source documentation
A uniformly 101-bounded representation on a separable Hilbert space, not similar to a unitary representation, constructed from nonamenability.
```
theorem nonamenable_witness (hG : ¬ Amenable G) : NonamenableWitness.{u,u} G := by
…
```
Mentions: OAI.Dixmier.Amenable
theorem OAI.Dixmier.main_theorem line 86
Source documentation
The conclusion at the common group/Hilbert-space universe.
```
theorem main_theorem : MainTheorem.{u,u} := by
…
```
theorem OAI.Dixmier.amenable_of_unitarizable line 91
Source documentation
Unitarizability implies amenability, without a common similarity bound.
```
theorem amenable_of_unitarizable (hG : Unitarizable.{u,u} G) : Amenable G := by
…
```
Mentions: OAI.Dixmier.Amenable