OAI/Computability/BinPacking/PCP/SourceAmplification.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGames.Integration.SourceParameters.rate line 9
  2. theorem OAI.BinPackingGames.Integration.SourceParameters.rate_bounds line 11
  3. theorem OAI.BinPackingGames.Integration.SourceParameters.fourth_power_comparison line 17
  4. theorem OAI.BinPackingGames.Integration.SourceParameters.four_bit_rate_comparison line 33
  5. theorem OAI.BinPackingGames.Integration.SourceParameters.logTwo_sixteen line 48
  6. theorem OAI.BinPackingGames.Integration.SourceParameters.game_repetition_rate line 54
  7. def OAI.BinPackingGames.Integration.SourceParameters.sourceThreshold line 72
  8. theorem OAI.BinPackingGames.Integration.SourceParameters.sourceThreshold_pos line 74
  9. theorem OAI.BinPackingGames.Integration.SourceParameters.exists_repetition_length line 79
  10. def OAI.BinPackingGames.Integration.SourceParameters.repetitionLength line 85
  11. theorem OAI.BinPackingGames.Integration.SourceParameters.repetitionLength_spec line 89
  12. theorem OAI.BinPackingGames.Integration.SourceParameters.repetitionLength_real_bound line 95
  13. theorem OAI.BinPackingCompleteness.SourceAmplification.logTwo_le_four line 112
  14. theorem OAI.BinPackingCompleteness.SourceAmplification.game_repetition_rate_le_sixteen line 121
  15. def OAI.BinPackingCompleteness.SourceAmplification.ClauseGap line 139
  16. theorem OAI.BinPackingCompleteness.SourceAmplification.source_value_le line 143
  17. theorem OAI.BinPackingCompleteness.SourceAmplification.source_repetition_rate line 157
  18. theorem OAI.BinPackingCompleteness.SourceAmplification.exists_repetition_length line 171
  19. def OAI.BinPackingCompleteness.SourceAmplification.repetitionLength line 180
  20. theorem OAI.BinPackingCompleteness.SourceAmplification.repetitionLength_spec line 183
  21. theorem OAI.BinPackingCompleteness.SourceAmplification.repeated_source_value_lt line 188
  22. theorem OAI.BinPackingCompleteness.SourceAmplification.repeated_completeness_success line 197
  23. theorem OAI.BinPackingCompleteness.SourceAmplification.repeated_completeness_value line 208