OAI/Computability/MinUncut/PCP/Bounds.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBounds.formulaBits_length line 12
  2. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBounds.formulaBits_length_ge_variables line 20
  3. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBounds.formulaBits_length_ge_clauses line 25
  4. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBounds.formulaBits_length_ge_two line 30
  5. def OAI.MinUncutGames.Foundations.Hastad.SourceBounds.bitCountFormula line 35
  6. def OAI.MinUncutGames.Foundations.Hastad.SourceBounds.bitCoefficient line 38
  7. def OAI.MinUncutGames.Foundations.Hastad.SourceBounds.testCoefficient line 40
  8. def OAI.MinUncutGames.Foundations.Hastad.SourceBounds.occurrenceCoefficient line 43
  9. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBounds.one_le_input_power line 45
  10. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBounds.bitCountFormula_le_input line 51
  11. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBounds.testCountFormula_le_input line 66
  12. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBounds.testCountFormula_add_one_le_input line 76
  13. def OAI.MinUncutGames.Foundations.Hastad.SourceBounds.sourceSizeBound line 85
  14. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBounds.sourceBits_length_le line 88
  15. def OAI.MinUncutGames.Foundations.Hastad.SourceBounds.sourcePolynomial line 98
  16. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBounds.sourcePolynomial_eval line 103
  17. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBounds.card_testTape line 110
  18. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBounds.testTapeEncoding_size line 115
  19. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBounds.card_sourceIndex line 119
  20. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBounds.nBits_le_input line 126
  21. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBounds.rawSourceList_length_eq line 131
  22. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBounds.rawSourceList_length_le_input line 137
  23. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBounds.sourceList_length_le_input line 144
  24. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBounds.sourceInput_bits_polynomial line 154
  25. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBounds.fixed_parameters_source_size line 162