UniverseTransport.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Countability lets a group be represented in any universe. Transport by group equivalences preserves the positive normalized invariant mean and the bounded nonunitarizable witness.

def OAI.Dixmier.meanPullback line 18
theorem OAI.Dixmier.meanPullback_apply line 24
theorem OAI.Dixmier.amenable_of_mulEquiv line 28
Source documentation
Amenability transport uses the same positive normalized invariant mean.
```
theorem amenable_of_mulEquiv (e : G ≃* Q) (hQ : Amenable Q) : Amenable G := by
…
```
Mentions: OAI.Dixmier.Amenable
theorem OAI.Dixmier.witness_of_mulEquiv line 44
Source documentation
Reindexing the group does not change the Hilbert space, bound or similarities.
```
theorem witness_of_mulEquiv (e : G ≃* Q) (hQ : NonamenableWitness.{v,w} Q) :
    NonamenableWitness.{u,w} G := by
…
```
theorem OAI.Dixmier.main_theorem_all_universes line 55
Source documentation
The main theorem with independent group and Hilbert-space universes.
Distinct definitions of this name: ComparatorChallenges/Dixmier.lean:44 (same statement text; different proof or body). Qualify references as OAI.Dixmier.main_theorem_all_universes@path.
```
theorem main_theorem_all_universes : MainTheorem.{u,v} := by
…
```
theorem OAI.Dixmier.amenable_of_unitarizable_all_universes line 66
Source documentation
Unitarizability implies amenability, with no uniform similarity bound.
```
theorem amenable_of_unitarizable_all_universes [Countable G]
    (h : Unitarizable.{u,v} G) : Amenable G := by
…
```
Mentions: OAI.Dixmier.Amenable