OAI/Combinatorics/SharpRamsey/Entropy/AnchorEventsRealized.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

High moments, finite-field subspaces, and incidence bounds.

  1. lemma OAI.SharpRamseyFive.ResidualCertificate.anchorEvents_realized line 22
  2. theorem OAI.SharpRamseyFive.ResidualCertificate.anchor_step_witnesses line 31
  3. def OAI.SharpRamseyFive.ResidualCertificate.pairEvents line 61
  4. lemma OAI.SharpRamseyFive.ResidualCertificate.pairEvents_card line 65
  5. lemma OAI.SharpRamseyFive.ResidualCertificate.pairEvents_realized line 73
  6. theorem OAI.SharpRamseyFive.ResidualCertificate.pair_step_witnesses line 81
  7. inductive OAI.SharpRamseyFive.ResidualCertificate.PaidStep line 117
  8. lemma OAI.SharpRamseyFive.ResidualCertificate.paidStep_realized line 131
  9. lemma OAI.SharpRamseyFive.ResidualCertificate.paidStep_dictionary line 141
  10. lemma OAI.SharpRamseyFive.ResidualCertificate.paidStep_cost line 166
  11. lemma OAI.SharpRamseyFive.ResidualCertificate.encodingStep_lift line 185
  12. lemma OAI.SharpRamseyFive.ResidualCertificate.encoding_path_lift line 201
  13. lemma OAI.SharpRamseyFive.ResidualCertificate.paid_path_cost line 216
  14. theorem OAI.SharpRamseyFive.ResidualCertificate.terminal_paid_certificate line 228
  15. def OAI.SharpRamseyFive.CertificateCover.Agrees line 266
  16. lemma OAI.SharpRamseyFive.CertificateCover.agrees_update line 270
  17. def OAI.SharpRamseyFive.CertificateCover.anchorName line 280
  18. lemma OAI.SharpRamseyFive.CertificateCover.anchorName_direction line 286
  19. lemma OAI.SharpRamseyFive.CertificateCover.anchorName_realized line 292
  20. lemma OAI.SharpRamseyFive.CertificateCover.anchor_req_card line 299
  21. lemma OAI.SharpRamseyFive.CertificateCover.anchor_req_directions line 304
  22. lemma OAI.SharpRamseyFive.CertificateCover.anchor_req_disjoint line 309
  23. lemma OAI.SharpRamseyFive.CertificateCover.rawCost_eq_weight line 320
  24. lemma OAI.SharpRamseyFive.CertificateCover.newEvents_card line 339
  25. def OAI.SharpRamseyFive.CertificateCover.Enabled line 355
  26. lemma OAI.SharpRamseyFive.CertificateCover.step_weight line 361
  27. def OAI.SharpRamseyFive.CertificateCover.Coherent line 371
  28. lemma OAI.SharpRamseyFive.CertificateCover.coherent_step line 378
  29. lemma OAI.SharpRamseyFive.CertificateCover.touched_anchor line 400
  30. lemma OAI.SharpRamseyFive.CertificateCover.make_one line 416
  31. lemma OAI.SharpRamseyFive.CertificateCover.make_two line 441