OAI/Computability/VertexCover/Fourier/SourceBounds.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniqueGames.Foundations.Hastad.SourceBounds.formulaBits_length line 44
  2. theorem OAI.UniqueGames.Foundations.Hastad.SourceBounds.formulaBits_length_ge_variables line 52
  3. theorem OAI.UniqueGames.Foundations.Hastad.SourceBounds.formulaBits_length_ge_clauses line 57
  4. theorem OAI.UniqueGames.Foundations.Hastad.SourceBounds.formulaBits_length_ge_two line 62
  5. def OAI.UniqueGames.Foundations.Hastad.SourceBounds.bitCountFormula line 67
  6. def OAI.UniqueGames.Foundations.Hastad.SourceBounds.bitCoefficient line 70
  7. def OAI.UniqueGames.Foundations.Hastad.SourceBounds.testCoefficient line 72
  8. def OAI.UniqueGames.Foundations.Hastad.SourceBounds.occurrenceCoefficient line 75
  9. theorem OAI.UniqueGames.Foundations.Hastad.SourceBounds.one_le_input_power line 77
  10. theorem OAI.UniqueGames.Foundations.Hastad.SourceBounds.bitCountFormula_le_input line 83
  11. theorem OAI.UniqueGames.Foundations.Hastad.SourceBounds.testCountFormula_le_input line 98
  12. theorem OAI.UniqueGames.Foundations.Hastad.SourceBounds.testCountFormula_add_one_le_input line 108
  13. def OAI.UniqueGames.Foundations.Hastad.SourceBounds.sourceSizeBound line 117
  14. theorem OAI.UniqueGames.Foundations.Hastad.SourceBounds.sourceBits_length_le line 120
  15. def OAI.UniqueGames.Foundations.Hastad.SourceBounds.sourcePolynomial line 130
  16. theorem OAI.UniqueGames.Foundations.Hastad.SourceBounds.sourcePolynomial_eval line 135
  17. theorem OAI.UniqueGames.Foundations.Hastad.SourceBounds.card_testTape line 142
  18. theorem OAI.UniqueGames.Foundations.Hastad.SourceBounds.testTapeEncoding_size line 147
  19. theorem OAI.UniqueGames.Foundations.Hastad.SourceBounds.card_sourceIndex line 151
  20. theorem OAI.UniqueGames.Foundations.Hastad.SourceBounds.nBits_le_input line 158
  21. theorem OAI.UniqueGames.Foundations.Hastad.SourceBounds.rawSourceList_length_eq line 163
  22. theorem OAI.UniqueGames.Foundations.Hastad.SourceBounds.rawSourceList_length_le_input line 169
  23. theorem OAI.UniqueGames.Foundations.Hastad.SourceBounds.sourceList_length_le_input line 176
  24. theorem OAI.UniqueGames.Foundations.Hastad.SourceBounds.sourceInput_bits_polynomial line 186
  25. theorem OAI.UniqueGames.Foundations.Hastad.SourceBounds.fixed_parameters_source_size line 194