OAI/Computability/UniqueGames/Analysis/A5IndexCount.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The actual forward Appendix A.5 index injects into two spaces of linear maps. The first map recovers the image complement, the second its kernel complement. No index-cardinality inequality is assumed.

  1. def OAI.UniqueGamesTheorem.Appendix.A5IndexCount.insideEquiv line 21
  2. theorem OAI.UniqueGamesTheorem.Appendix.A5IndexCount.internal_isCompl line 30
  3. def OAI.UniqueGamesTheorem.Appendix.A5IndexCount.projectionA0 line 47
  4. theorem OAI.UniqueGamesTheorem.Appendix.A5IndexCount.projectionA0_injective line 53
  5. def OAI.UniqueGamesTheorem.Appendix.A5IndexCount.fullRange line 83
  6. theorem OAI.UniqueGamesTheorem.Appendix.A5IndexCount.fullRange_surjective line 88
  7. theorem OAI.UniqueGamesTheorem.Appendix.A5IndexCount.quotientRestriction_surjective line 92
  8. theorem OAI.UniqueGamesTheorem.Appendix.A5IndexCount.quotientRestriction_same_kernel line 103
  9. def OAI.UniqueGamesTheorem.Appendix.A5IndexCount.sectionB0 line 117
  10. theorem OAI.UniqueGamesTheorem.Appendix.A5IndexCount.range_sectionB0 line 125
  11. theorem OAI.UniqueGamesTheorem.Appendix.A5IndexCount.recover_sectionB0 line 132
  12. theorem OAI.UniqueGamesTheorem.Appendix.A5IndexCount.sectionB0_injective line 150
  13. def OAI.UniqueGamesTheorem.Appendix.A5IndexCount.encode line 161
  14. theorem OAI.UniqueGamesTheorem.Appendix.A5IndexCount.encode_injective line 167
  15. theorem OAI.UniqueGamesTheorem.Appendix.A5IndexCount.card_geometricIndex_le line 180
  16. theorem OAI.UniqueGamesTheorem.Appendix.A5IndexCount.card_geometricIndex_degree_le line 199
  17. theorem OAI.UniqueGamesTheorem.Appendix.A5IndexCount.card_geometricIndex_cube_le line 214