OAI/Computability/VertexCover/PCP/PoweringCounting.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniqueGames.Foundations.PCP.PoweringCounting.constraint_rejection_mean_eq_count line 16
  2. theorem OAI.UniqueGames.Foundations.PCP.PoweringCounting.constraint_rejection_lower_iff line 31
  3. theorem OAI.UniqueGames.Foundations.PCP.PoweringCounting.edgeDensity_eq_bit_mean line 40
  4. theorem OAI.UniqueGames.Foundations.PCP.PoweringCounting.base_edgeDensity_eq_rejection_count line 54
  5. theorem OAI.UniqueGames.Foundations.PCP.PoweringCounting.base_count_lower_to_density line 72
  6. theorem OAI.UniqueGames.Foundations.PCP.PoweringCounting.powered_rejection_mean_eq_count line 82
  7. theorem OAI.UniqueGames.Foundations.PCP.PoweringCounting.path_rejection_mean_eq_count line 92
  8. theorem OAI.UniqueGames.Foundations.PCP.PoweringCounting.powered_density_lower_to_count line 103
  9. theorem OAI.UniqueGames.Foundations.PCP.PoweringCounting.natCard_dart line 115
  10. theorem OAI.UniqueGames.Foundations.PCP.PoweringCounting.fintypeCard_dart line 119
  11. theorem OAI.UniqueGames.Foundations.PCP.PoweringCounting.natCard_poweredAlphabet line 124
  12. theorem OAI.UniqueGames.Foundations.PCP.PoweringCounting.natCard_finitePortAlphabet line 129