Model.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Amenability, unitarizability, and bounded nonunitarizable representations. Representations into the endomorphism monoid have bounded inverses because their domain is a group. Norm-preserving invertible complex linear maps on Hilbert spaces are unitary. No bound on similarities is imposed.

def OAI.Dixmier.leftTranslate line 16
Also declared: ComparatorChallenges/Dixmier.lean:12 (same declaration text), ComparatorChallenges/DixmierAllDiscrete.lean:12 (same declaration text).
def OAI.Dixmier.Amenable line 21
Source documentation
A positive normalized left-invariant complex mean.
Also declared: ComparatorChallenges/Dixmier.lean:17 (same declaration text), ComparatorChallenges/DixmierAllDiscrete.lean:16 (same declaration text).
```
def Amenable (G : Type u) [Group G] [TopologicalSpace G]
    [DiscreteTopology G] : Prop :=
…
```
def OAI.Dixmier.SimilarToUnitary line 29
Also declared: ComparatorChallenges/Dixmier.lean:25 (same declaration text), ComparatorChallenges/DixmierAllDiscrete.lean:24 (same declaration text).
def OAI.Dixmier.NonamenableWitness line 36
Source documentation
A uniformly 101-bounded nonunitarizable representation on a separable complete complex Hilbert space, with its universe explicit.
Also declared: ComparatorChallenges/Dixmier.lean:32 (same declaration text).
```
def NonamenableWitness (G : Type u) [Group G] : Prop :=
…
```
def OAI.Dixmier.Unitarizable line 43
Source documentation
Unitarizability at an explicitly quantified Hilbert-space universe.
Also declared: ComparatorChallenges/DixmierAllDiscrete.lean:29 (same declaration text).
```
def Unitarizable (G : Type u) [Group G] : Prop :=
…
```
def OAI.Dixmier.MainTheorem line 49
Source documentation
Every countable discrete nonamenable group has a bounded nonunitarizable witness.
Also declared: ComparatorChallenges/Dixmier.lean:39 (same declaration text).
```
def MainTheorem : Prop :=
…
```

theorem OAI.Dixmier.witness_not_unitarizable line 54

Source documentation

A nonunitarizable witness contradicts unitarizability.

theorem witness_not_unitarizable {G : Type u} [Group G]
    (h : NonamenableWitness.{u, v} G) : ¬ Unitarizable.{u, v} G := by
…