OAI/Combinatorics/SharpRamsey/Marking/Popular.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SharpLogRamsey.Marking.popular_zero line 15
  2. theorem OAI.SharpLogRamsey.Marking.popular_card line 39
  3. def OAI.SharpLogRamsey.Marking.partnerDomain line 81
  4. theorem OAI.SharpLogRamsey.Marking.partner_card line 86
  5. def OAI.SharpLogRamsey.Marking.popularJoint line 100
  6. theorem OAI.SharpLogRamsey.Marking.popular_joint_card line 105
  7. inductive OAI.SharpLogRamsey.Marking.ScanKind line 147
  8. instance OAI.SharpLogRamsey.Marking.flat_ActualMarkingOrientation_1 line 151
  9. def OAI.SharpLogRamsey.Marking.levelFromRank line 155
  10. lemma OAI.SharpLogRamsey.Marking.chosenLevel_from_rank line 160
  11. abbrev OAI.SharpLogRamsey.Marking.RankMask line 163
  12. abbrev OAI.SharpLogRamsey.Marking.ScanFlag line 165
  13. def OAI.SharpLogRamsey.Marking.flagKind line 167
  14. lemma OAI.SharpLogRamsey.Marking.flagKind_expensive line 172
  15. def OAI.SharpLogRamsey.Marking.maskAt line 177
  16. def OAI.SharpLogRamsey.Marking.sentAt line 181
  17. def OAI.SharpLogRamsey.Marking.replayStep line 184
  18. def OAI.SharpLogRamsey.Marking.markingCode line 189
  19. def OAI.SharpLogRamsey.Marking.replay line 195
  20. lemma OAI.SharpLogRamsey.Marking.markingCode_length line 200
  21. theorem OAI.SharpLogRamsey.Marking.replay_markingCode line 206
  22. def OAI.SharpLogRamsey.Marking.decodedCheap line 216
  23. lemma OAI.SharpLogRamsey.Marking.decodedCheap_maskAt line 224
  24. lemma OAI.SharpLogRamsey.Marking.mask_records_transmission line 239
  25. lemma OAI.SharpLogRamsey.Marking.rankMask_card line 246
  26. def OAI.SharpLogRamsey.Marking.ScanConsistent line 260
  27. lemma OAI.SharpLogRamsey.Marking.update_annihilates_later line 265
  28. def OAI.SharpLogRamsey.Marking.validCode line 276
  29. theorem OAI.SharpLogRamsey.Marking.markingCode_valid line 284
  30. theorem OAI.SharpLogRamsey.Marking.markingCode_valid_zero line 304
  31. lemma OAI.SharpLogRamsey.Marking.levelFromRank_spec line 310
  32. abbrev OAI.SharpLogRamsey.Marking.ProjectivePair line 327
  33. def OAI.SharpLogRamsey.Marking.incidentPairs line 329
  34. lemma OAI.SharpLogRamsey.Marking.incidentPairs_card line 335
  35. def OAI.SharpLogRamsey.Marking.projectiveCheapDomain line 341
  36. lemma OAI.SharpLogRamsey.Marking.cheapDomain_membership line 351
  37. lemma OAI.SharpLogRamsey.Marking.popularJoint_empty_of_level_empty line 377
  38. theorem OAI.SharpLogRamsey.Marking.projectiveCheapDomain_card line 388
  39. def OAI.SharpLogRamsey.ProjectiveDuality.mapEquiv line 420
  40. def OAI.SharpLogRamsey.ProjectiveDuality.bidual line 431
  41. lemma OAI.SharpLogRamsey.ProjectiveDuality.incident_bidual line 434
  42. def OAI.SharpLogRamsey.Incident line 452
  43. structure OAI.SharpLogRamsey.Flag line 454
  44. def OAI.SharpLogRamsey.Consistent line 459
  45. def OAI.SharpLogRamsey.Marking.forwardScan line 472
  46. def OAI.SharpLogRamsey.Marking.backwardScan line 476
  47. theorem OAI.SharpLogRamsey.Marking.forwardScan_consistent line 479
  48. theorem OAI.SharpLogRamsey.Marking.backwardScan_consistent line 489
  49. theorem OAI.SharpLogRamsey.Marking.forward_own_incident line 495
  50. theorem OAI.SharpLogRamsey.Marking.forwardScan_valid line 502
  51. theorem OAI.SharpLogRamsey.Marking.backwardScan_valid line 508