OAI/Combinatorics/IndependentSets/Encoding/Bounds.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.formulaBits_length line 11
  2. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.formulaBits_length_ge_variables line 19
  3. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.formulaBits_length_ge_clauses line 24
  4. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.formulaBits_length_ge_two line 29
  5. def OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.bitCountFormula line 34
  6. def OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.bitCoefficient line 37
  7. def OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.testCoefficient line 39
  8. def OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.occurrenceCoefficient line 42
  9. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.one_le_input_power line 44
  10. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.bitCountFormula_le_input line 50
  11. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.testCountFormula_le_input line 65
  12. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.testCountFormula_add_one_le_input line 75
  13. def OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.sourceSizeBound line 84
  14. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.sourceBits_length_le line 87
  15. def OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.sourcePolynomial line 97
  16. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.sourcePolynomial_eval line 102
  17. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.card_testTape line 109
  18. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.testTapeEncoding_size line 114
  19. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.card_sourceIndex line 118
  20. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.nBits_le_input line 125
  21. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.rawSourceList_length_eq line 130
  22. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.rawSourceList_length_le_input line 136
  23. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.sourceList_length_le_input line 143
  24. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.sourceInput_bits_polynomial line 153
  25. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceBounds.fixed_parameters_source_size line 161