OAI/Combinatorics/IndependentSets/Expansion/PoweringNumeric.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringNumeric.min_density_ratio line 10
2. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringNumeric.count_moment_ratio_lower line 36
3. def OAI.IndependentSetsGames.Foundations.PCP.PoweringSoundness.center line 71
4. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringSoundness.le_center line 73
5. def OAI.IndependentSetsGames.Foundations.PCP.PoweringSoundness.gain line 81
6. def OAI.IndependentSetsGames.Foundations.PCP.PoweringSoundness.decodedError line 88
7. def OAI.IndependentSetsGames.Foundations.PCP.PoweringSoundness.poweredRejection line 93
8. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringSoundness.witness_bit_eq line 99
9. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringSoundness.modal_witness_mean line 112
10. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringSoundness.rejection_lower_bound line 137