OAI/Computability/VertexCover/PCP/PoweringMoment.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.PCP.PoweringMoment.bit line 11
2. def OAI.UniqueGames.Foundations.PCP.PoweringMoment.hits line 15
3. def OAI.UniqueGames.Foundations.PCP.PoweringMoment.mean line 18
4. theorem OAI.UniqueGames.Foundations.PCP.PoweringMoment.bit_nonneg line 20
5. theorem OAI.UniqueGames.Foundations.PCP.PoweringMoment.bit_sq line 24
6. theorem OAI.UniqueGames.Foundations.PCP.PoweringMoment.bit_mul line 28
7. theorem OAI.UniqueGames.Foundations.PCP.PoweringMoment.bit_mono line 32
8. theorem OAI.UniqueGames.Foundations.PCP.PoweringMoment.hits_nonneg line 40
9. theorem OAI.UniqueGames.Foundations.PCP.PoweringMoment.mean_nonneg line 43
10. theorem OAI.UniqueGames.Foundations.PCP.PoweringMoment.mean_hits line 46
11. theorem OAI.UniqueGames.Foundations.PCP.PoweringMoment.second_moment_eq line 50
12. theorem OAI.UniqueGames.Foundations.PCP.PoweringMoment.mean_witness_sq_le line 58
13. theorem OAI.UniqueGames.Foundations.PCP.PoweringMoment.rejection_lower_bound line 90