OAI/Combinatorics/IndependentSets/Expansion/CayleyTailCount.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.upperMasks line 14
  2. def OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.lowerMasks line 17
  3. def OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.badMasks line 20
  4. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.upperMasks_weight line 25
  5. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.lowerMasks_complement_image line 42
  6. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.lowerMasks_card_eq_upperMasks line 65
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.ratio_le_of_weight line 79
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.upperMasks_ratio_le line 93
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.lowerMasks_ratio_le line 98
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.badMasks_ratio_le_sharp line 103
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.badMasks_ratio_le line 118
  12. def OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.trueMask line 128
  13. def OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.countTrue line 131
  14. def OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.badWord line 133
  15. instance OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.(instance at line 136) line 136
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.bitSign_mean_eq line 139
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.not_badWord_bias line 155
  18. def OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.wordMaskEquiv line 175
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.twoTail_probability line 185
  20. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.union_bound_le_half line 206
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.fixed_parameters line 223
  22. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.fixed_union_bound line 226
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.seventh_power_size line 230
  24. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleyTailCount.seventh_power_abs_le line 233