OAI/Analysis/Cotype/EquivariantPairing.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Cotype.finiteProbabilityVector line 16
  2. def OAI.Cotype.finiteProbabilityDual line 19
  3. theorem OAI.Cotype.finiteProbabilityVector_norm line 22
  4. theorem OAI.Cotype.finiteProbabilityDual_norm line 39
  5. abbrev OAI.Cotype.SymmetryL2 line 48
  6. def OAI.Cotype.symmetryVector line 50
  7. def OAI.Cotype.symmetryDual line 53
  8. theorem OAI.Cotype.symmetryVector_equivariant line 56
  9. theorem OAI.Cotype.symmetryDual_equivariant line 61
  10. theorem OAI.Cotype.symmetry_exact_pairing line 76
  11. theorem OAI.Cotype.symmetry_pairing_invariant line 90
  12. theorem OAI.Cotype.exists_equivariant_exact_pairing line 98