OAI/Combinatorics/IndependentSets/PCP/TableIteration.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.TableIteration.run line 13
2. def OAI.IndependentSetsGames.Foundations.PCP.TableIteration.runTables line 15
3. theorem OAI.IndependentSetsGames.Foundations.PCP.TableIteration.run_val line 18
4. def OAI.IndependentSetsGames.Foundations.PCP.TableIteration.iterationCount line 26
5. def OAI.IndependentSetsGames.Foundations.PCP.TableIteration.output line 28
6. def OAI.IndependentSetsGames.Foundations.PCP.TableIteration.outputTable line 30
7. theorem OAI.IndependentSetsGames.Foundations.PCP.TableIteration.output_val line 33
8. def OAI.IndependentSetsGames.Foundations.PCP.TableIteration.gapMap line 36
9. opaque OAI.IndependentSetsGames.Foundations.PCP.TableIteration.degreeData line 38
10. def OAI.IndependentSetsGames.Foundations.PCP.TableIteration.polynomialDegree line 41
11. theorem OAI.IndependentSetsGames.Foundations.PCP.TableIteration.sizeFactor_le_power line 43
12. theorem OAI.IndependentSetsGames.Foundations.PCP.TableIteration.run_completeness line 46
13. theorem OAI.IndependentSetsGames.Foundations.PCP.TableIteration.output_completeness line 50
14. theorem OAI.IndependentSetsGames.Foundations.PCP.TableIteration.gapMap_completeness line 54
15. theorem OAI.IndependentSetsGames.Foundations.PCP.TableIteration.output_darts_positive line 60
16. theorem OAI.IndependentSetsGames.Foundations.PCP.TableIteration.gapMap_nonempty line 64
17. theorem OAI.IndependentSetsGames.Foundations.PCP.TableIteration.run_size line 67
18. theorem OAI.IndependentSetsGames.Foundations.PCP.TableIteration.output_size line 71
19. theorem OAI.IndependentSetsGames.Foundations.PCP.TableIteration.initial_size_le line 76
20. theorem OAI.IndependentSetsGames.Foundations.PCP.TableIteration.output_size_le_input line 79
21. def OAI.IndependentSetsGames.Foundations.PCP.TableIteration.tableSizePolynomial line 87
22. theorem OAI.IndependentSetsGames.Foundations.PCP.TableIteration.tableSizePolynomial_eval line 90
23. def OAI.IndependentSetsGames.Foundations.PCP.TableIteration.tableBitsPolynomial line 95
24. theorem OAI.IndependentSetsGames.Foundations.PCP.TableIteration.output_bits_le line 98
25. def OAI.IndependentSetsGames.Foundations.PCP.TableIteration.formulaBitsPolynomial line 103
26. theorem OAI.IndependentSetsGames.Foundations.PCP.TableIteration.gapMap_bits_le line 106