OAI/Probability/SignedSweeps/ColumnSubgroup.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedSweeps.oneCardRepresentation line 12
  2. lemma OAI.SignedSweeps.oneCardRepresentation_apply line 22
  3. def OAI.SignedSweeps.binaryFlip line 25
  4. def OAI.SignedSweeps.flipPermutation line 31
  5. lemma OAI.SignedSweeps.binaryFlip_apply line 35
  6. lemma OAI.SignedSweeps.flipPermutation_inv line 39
  7. lemma OAI.SignedSweeps.flipPermutation_twice line 46
  8. lemma OAI.SignedSweeps.flipPermutation_mem line 52
  9. lemma OAI.SignedSweeps.flipPermutation_commute line 58
  10. lemma OAI.SignedSweeps.binary_eq_or_flip line 71
  11. lemma OAI.SignedSweeps.coordinate_or_flip line 87
  12. lemma OAI.SignedSweeps.oneCard_average_eq line 98
  13. lemma OAI.SignedSweeps.oneCard_averages_commute line 123
  14. lemma OAI.SignedSweeps.prod_absorbs_commuting_idempotent line 133
  15. def OAI.SignedSweeps.oneCardSweep line 146
  16. lemma OAI.SignedSweeps.oneCardSweep_invariant line 150
  17. lemma OAI.SignedSweeps.oneCard_sum_invariant line 173
  18. lemma OAI.SignedSweeps.oneCard_average_sum line 177
  19. lemma OAI.SignedSweeps.oneCardSweep_sum line 186
  20. lemma OAI.SignedSweeps.oneCardSweep_uniform line 201
  21. def OAI.SignedSweeps.oneCardLift line 212
  22. lemma OAI.SignedSweeps.oneCardLift_intertwines line 217
  23. lemma OAI.SignedSweeps.oneCardLift_groupAverage line 222
  24. lemma OAI.SignedSweeps.spechtInclusion_layer line 229
  25. lemma OAI.SignedSweeps.specht_function_of_one_card line 237
  26. lemma OAI.SignedSweeps.oneCardLift_sweep line 253
  27. lemma OAI.SignedSweeps.sweepOperator_eq_zero_of_level_one line 270
  28. lemma OAI.SignedSweeps.weightedMoment_eq_zero_of_level_one line 285
  29. lemma OAI.SignedSweeps.signed_moment_bound_of_level_one line 291