OAI/Combinatorics/SharpRamsey/Marking/MarkingOrientation.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpLogRamsey.Marking.level line 14
  2. def OAI.SharpLogRamsey.Marking.below line 15
  3. def OAI.SharpLogRamsey.Marking.potential line 16
  4. theorem OAI.SharpLogRamsey.Marking.below_antitone line 19
  5. theorem OAI.SharpLogRamsey.Marking.potential_nonneg line 25
  6. theorem OAI.SharpLogRamsey.Marking.potential_le line 31
  7. theorem OAI.SharpLogRamsey.Marking.log_drop line 41
  8. theorem OAI.SharpLogRamsey.Marking.potential_drop line 54
  9. theorem OAI.SharpLogRamsey.Marking.below_card_le_of_max line 72
  10. abbrev OAI.SharpLogRamsey.Marking.Points line 90
  11. abbrev OAI.SharpLogRamsey.Marking.State line 91
  12. def OAI.SharpLogRamsey.Marking.ranks line 92
  13. def OAI.SharpLogRamsey.Marking.update line 95
  14. theorem OAI.SharpLogRamsey.Marking.le_update line 100
  15. theorem OAI.SharpLogRamsey.Marking.ranks_update_mono line 108
  16. theorem OAI.SharpLogRamsey.Marking.ranks_lt_update line 113
  17. def OAI.SharpLogRamsey.Marking.Popular line 124
  18. def OAI.SharpLogRamsey.Marking.Poor line 129
  19. theorem OAI.SharpLogRamsey.Marking.expensive_drop line 134
  20. def OAI.SharpLogRamsey.Marking.chosenLevel line 209
  21. theorem OAI.SharpLogRamsey.Marking.chosenLevel_spec line 215
  22. def OAI.SharpLogRamsey.Marking.IsExpensive line 223
  23. def OAI.SharpLogRamsey.Marking.scan line 227
  24. theorem OAI.SharpLogRamsey.Marking.scan_potential_bound line 236
  25. theorem OAI.SharpLogRamsey.Marking.scan_expensive_bound line 257
  26. theorem OAI.SharpLogRamsey.Marking.update_le_ker line 274
  27. def OAI.SharpLogRamsey.Marking.historyState line 285
  28. theorem OAI.SharpLogRamsey.Marking.historyState_le_ker line 290
  29. theorem OAI.SharpLogRamsey.Marking.historyState_rank_bound line 302
  30. theorem OAI.SharpLogRamsey.Marking.geom_sum_le_twice line 320
  31. theorem OAI.SharpLogRamsey.Marking.card_subspace_points_le line 331
  32. theorem OAI.SharpLogRamsey.Marking.joint_bound_of_product line 345
  33. def OAI.SharpLogRamsey.Marking.poorDomain line 392
  34. theorem OAI.SharpLogRamsey.Marking.poor_marginal_product line 396
  35. theorem OAI.SharpLogRamsey.Marking.poor_joint_domain_bound line 417
  36. def OAI.SharpLogRamsey.Marking.popularDomain line 436