OAI/Computability/BinPacking/Games/AlphabetBudget.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGames.Foundations.Repetition.logTwo line 15
  2. theorem OAI.BinPackingGames.Foundations.Repetition.logTwo_one line 17
  3. theorem OAI.BinPackingGames.Foundations.Repetition.logTwo_inv_le_of_half_pow_le line 19
  4. theorem OAI.BinPackingGames.Foundations.Repetition.contraction_step line 31
  5. theorem OAI.BinPackingGames.Foundations.Repetition.initial_step line 70
  6. theorem OAI.BinPackingGames.Foundations.Repetition.cutoff_step line 75
  7. theorem OAI.BinPackingGames.Foundations.Repetition.cutoff_le_length line 87
  8. def OAI.BinPackingGames.Foundations.Repetition.ScalarRecurrence line 95
  9. theorem OAI.BinPackingGames.Foundations.Repetition.decay_to_cutoff line 99
  10. theorem OAI.BinPackingGames.Foundations.Repetition.block_contraction line 136
  11. theorem OAI.BinPackingGames.Foundations.Repetition.scalar_bound_6000 line 148
  12. def OAI.BinPackingGames.Foundations.Repetition.incidenceRate line 171
  13. theorem OAI.BinPackingGames.Foundations.Repetition.incidenceRate_pos line 173
  14. theorem OAI.BinPackingGames.Foundations.Repetition.incidenceRate_lt_one line 175
  15. theorem OAI.BinPackingGames.Foundations.Repetition.incidenceRate_fourth line 177
  16. theorem OAI.BinPackingGames.Foundations.Repetition.incidence_rate_comparison line 181
  17. theorem OAI.BinPackingGames.Foundations.Repetition.scalar_incidence_bound line 192
  18. theorem OAI.BinPackingGames.Foundations.Repetition.SelectionSequence.exists_unused line 212
  19. def OAI.BinPackingGames.Foundations.Repetition.SelectionSequence.nextSet line 228
  20. def OAI.BinPackingGames.Foundations.Repetition.SelectionSequence.selectedSet line 234
  21. theorem OAI.BinPackingGames.Foundations.Repetition.SelectionSequence.selectedSet_card line 240
  22. theorem OAI.BinPackingGames.Foundations.Repetition.SelectionSequence.selectedSet_subset_succ line 263
  23. theorem OAI.BinPackingGames.Foundations.Repetition.SelectionSequence.selectedSet_monotone line 273
  24. theorem OAI.BinPackingGames.Foundations.Repetition.SelectionSequence.selectedSet_univ line 279
  25. theorem OAI.BinPackingGames.Foundations.Repetition.SelectionSequence.selectedSet_step line 286
  26. def OAI.BinPackingGames.Foundations.Repetition.SelectionSequence.SetStep line 301
  27. theorem OAI.BinPackingGames.Foundations.Repetition.SelectionSequence.totalSetStep line 307
  28. theorem OAI.BinPackingGames.Foundations.Repetition.SelectionSequence.exists_scalar_sequence line 322
  29. def OAI.BinPackingGames.Foundations.Repetition.SelectionSequence.ConditionalCoordinateBound line 355
  30. theorem OAI.BinPackingGames.Foundations.Repetition.SelectionSequence.repetition_success_le_of_conditionalCoordinateBound line 367
  31. theorem OAI.BinPackingGames.Foundations.Repetition.selectedLabels_card line 405
  32. theorem OAI.BinPackingGames.Foundations.Repetition.unusedCoordinates_card line 410
  33. theorem OAI.BinPackingGames.Foundations.Repetition.unusedCoordinates_card_real line 415
  34. theorem OAI.BinPackingGames.Foundations.Repetition.log_le_logTwo line 420
  35. theorem OAI.BinPackingGames.Foundations.Repetition.selectedLabels_log_le line 429
  36. theorem OAI.BinPackingGames.Foundations.Repetition.selectedInformationRadius_le line 441
  37. theorem OAI.BinPackingGames.Foundations.Repetition.sqrt_budget_factor line 460
  38. theorem OAI.BinPackingGames.Foundations.Repetition.exists_coordinate_le_information_budget line 467