OAI/Combinatorics/IndependentSets/Expansion/PoweringWitness.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWitness.iterate_mul_const line 15
2. def OAI.IndependentSetsGames.Foundations.PCP.PoweringWitness.endpointWitness line 28
3. def OAI.IndependentSetsGames.Foundations.PCP.PoweringWitness.vertexWitness line 34
4. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWitness.endpoint_lower_bound line 39
5. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWitness.lazy_middle_witness_mean line 74
6. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringMomentBound.symmetric_gap_matrix_sum line 113
7. def OAI.IndependentSetsGames.Foundations.PCP.PoweringMomentBound.windowIndex line 168
8. def OAI.IndependentSetsGames.Foundations.PCP.PoweringMomentBound.windowEvent line 173
9. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringMomentBound.window_second_moment_eq line 177
10. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringMomentBound.window_second_moment_le line 201