OAI/Computability/VertexCover/PCP/CayleyTailCount.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.PCP.CayleyTailCount.upperMasks line 15
  2. def OAI.UniqueGames.Foundations.PCP.CayleyTailCount.lowerMasks line 18
  3. def OAI.UniqueGames.Foundations.PCP.CayleyTailCount.badMasks line 21
  4. theorem OAI.UniqueGames.Foundations.PCP.CayleyTailCount.upperMasks_weight line 26
  5. theorem OAI.UniqueGames.Foundations.PCP.CayleyTailCount.lowerMasks_complement_image line 43
  6. theorem OAI.UniqueGames.Foundations.PCP.CayleyTailCount.lowerMasks_card_eq_upperMasks line 66
  7. theorem OAI.UniqueGames.Foundations.PCP.CayleyTailCount.ratio_le_of_weight line 80
  8. theorem OAI.UniqueGames.Foundations.PCP.CayleyTailCount.upperMasks_ratio_le line 94
  9. theorem OAI.UniqueGames.Foundations.PCP.CayleyTailCount.lowerMasks_ratio_le line 99
  10. theorem OAI.UniqueGames.Foundations.PCP.CayleyTailCount.badMasks_ratio_le_sharp line 104
  11. theorem OAI.UniqueGames.Foundations.PCP.CayleyTailCount.badMasks_ratio_le line 119
  12. def OAI.UniqueGames.Foundations.PCP.CayleyTailCount.trueMask line 129
  13. def OAI.UniqueGames.Foundations.PCP.CayleyTailCount.countTrue line 132
  14. def OAI.UniqueGames.Foundations.PCP.CayleyTailCount.badWord line 134
  15. instance OAI.UniqueGames.Foundations.PCP.CayleyTailCount.(instance at line 137) line 137
  16. theorem OAI.UniqueGames.Foundations.PCP.CayleyTailCount.bitSign_mean_eq line 140
  17. theorem OAI.UniqueGames.Foundations.PCP.CayleyTailCount.not_badWord_bias line 156
  18. def OAI.UniqueGames.Foundations.PCP.CayleyTailCount.wordMaskEquiv line 176
  19. theorem OAI.UniqueGames.Foundations.PCP.CayleyTailCount.twoTail_probability line 186
  20. theorem OAI.UniqueGames.Foundations.PCP.CayleyTailCount.union_bound_le_half line 207
  21. theorem OAI.UniqueGames.Foundations.PCP.CayleyTailCount.fixed_parameters line 224
  22. theorem OAI.UniqueGames.Foundations.PCP.CayleyTailCount.fixed_union_bound line 227
  23. theorem OAI.UniqueGames.Foundations.PCP.CayleyTailCount.seventh_power_size line 231
  24. theorem OAI.UniqueGames.Foundations.PCP.CayleyTailCount.seventh_power_abs_le line 234