OAI/Computability/UniqueGames/Analysis/OperatorPartitions.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Actual Fourier-projector partitions for Appendix A.4 and A.5

The partitions use the proved unique geometric selectors on each actual Fourier index. Their finite index types are the canonical counting types.

  1. theorem OAI.UniqueGamesTheorem.Appendix.OperatorPartitions.indicator_eq_sum_of_unique line 26
  2. theorem OAI.UniqueGamesTheorem.Appendix.OperatorPartitions.spectralProjector_partition line 53
  3. theorem OAI.UniqueGamesTheorem.Appendix.OperatorPartitions.spectralProjector_restriction_projector line 67
  4. abbrev OAI.UniqueGamesTheorem.Appendix.OperatorPartitions.A4Geometry line 87
  5. abbrev OAI.UniqueGamesTheorem.Appendix.OperatorPartitions.A4GeometricIndex line 90
  6. def OAI.UniqueGamesTheorem.Appendix.OperatorPartitions.a4Mask line 93
  7. theorem OAI.UniqueGamesTheorem.Appendix.OperatorPartitions.a4Mask_unique line 100
  8. theorem OAI.UniqueGamesTheorem.Appendix.OperatorPartitions.a4Mask_implies_weak line 115
  9. theorem OAI.UniqueGamesTheorem.Appendix.OperatorPartitions.a4_projector_partition line 123
  10. def OAI.UniqueGamesTheorem.Appendix.OperatorPartitions.A5Geometry line 130
  11. abbrev OAI.UniqueGamesTheorem.Appendix.OperatorPartitions.A5GeometricIndex line 135
  12. def OAI.UniqueGamesTheorem.Appendix.OperatorPartitions.a5Mask line 139
  13. def OAI.UniqueGamesTheorem.Appendix.OperatorPartitions.a5OuterMask line 144
  14. theorem OAI.UniqueGamesTheorem.Appendix.OperatorPartitions.a5Mask_unique line 151
  15. theorem OAI.UniqueGamesTheorem.Appendix.OperatorPartitions.a5Mask_implies_outer line 168
  16. theorem OAI.UniqueGamesTheorem.Appendix.OperatorPartitions.a5_projector_partition line 179