OAI/Analysis/Cotype/EquivariantLifts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Cotype.isometryAction_mul line 13
2. theorem OAI.Cotype.isometryAction_one line 17
3. def OAI.Cotype.orbitAverage line 20
4. theorem OAI.Cotype.orbitAverage_equivariant line 23
5. theorem OAI.Cotype.orbitAverage_norm_le_one line 31
6. theorem OAI.Cotype.orbitAverage_moment line 41
7. theorem OAI.Cotype.exists_equivariant_primal_lifts line 63
8. theorem OAI.Cotype.exists_equivariant_dual_lifts line 76