OAI/Combinatorics/IndependentSets/Expansion/PoweringTables.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.PCP.PoweringTables.labelCount line 13
  2. def OAI.IndependentSetsGames.Foundations.PCP.PoweringTables.dartCount line 15
  3. def OAI.IndependentSetsGames.Foundations.PCP.PoweringTables.mathematicalGraph line 17
  4. def OAI.IndependentSetsGames.Foundations.PCP.PoweringTables.rowAccepts line 23
  5. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTables.rowAccepts_eq line 32
  6. def OAI.IndependentSetsGames.Foundations.PCP.PoweringTables.table line 42
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTables.table_vertices line 47
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTables.table_darts line 50
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTables.semantics_table line 53
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTables.table_accepts line 59
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTables.table_reverse line 67
  12. def OAI.IndependentSetsGames.Foundations.PCP.PoweringTables.outputBits line 79
  13. def OAI.IndependentSetsGames.Foundations.PCP.PoweringTables.transform line 82
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringCounting.constraint_rejection_mean_eq_count line 93
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringCounting.constraint_rejection_lower_iff line 109
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringCounting.edgeDensity_eq_bit_mean line 118
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringCounting.base_edgeDensity_eq_rejection_count line 133
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringCounting.base_count_lower_to_density line 151
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringCounting.powered_rejection_mean_eq_count line 161
  20. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringCounting.path_rejection_mean_eq_count line 171
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringCounting.powered_density_lower_to_count line 182
  22. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringCounting.natCard_dart line 194
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringCounting.fintypeCard_dart line 198
  24. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringCounting.natCard_poweredAlphabet line 203
  25. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringCounting.natCard_finitePortAlphabet line 208