OAI/Probability/SignedSweeps/SwitchAverages.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedSweeps.realGroupAverage line 13
  2. lemma OAI.SignedSweeps.realGroupAverage_invariant line 16
  3. lemma OAI.SignedSweeps.realGroupAverage_fixed line 24
  4. lemma OAI.SignedSweeps.realGroupAverage_apply_action line 31
  5. def OAI.SignedSweeps.fairAction line 50
  6. lemma OAI.SignedSweeps.fairAction_apply line 53
  7. lemma OAI.SignedSweeps.action_absorbs_fairAction line 56
  8. lemma OAI.SignedSweeps.fairAction_idempotent line 63
  9. lemma OAI.SignedSweeps.fairActions_commute line 73
  10. def OAI.SignedSweeps.realVectorStabilizer line 81
  11. lemma OAI.SignedSweeps.fairAction_prod_fixed line 96
  12. lemma OAI.SignedSweeps.realGroupAverage_fairAction line 109
  13. lemma OAI.SignedSweeps.realGroupAverage_eq_fairAction_prod line 114
  14. lemma OAI.SignedSweeps.fiberSubgroup_le_of_swaps line 145
  15. lemma OAI.SignedSweeps.flipPermutation_ne line 185
  16. lemma OAI.SignedSweeps.coordinate_edge_swap_mem line 194
  17. lemma OAI.SignedSweeps.coordinateSubgroup_le_of_edge_swaps line 199
  18. lemma OAI.SignedSweeps.coordinate_edge_swaps_commute line 214
  19. lemma OAI.SignedSweeps.coordinate_real_average_as_switches line 234