OAI/Combinatorics/SharpRamsey/Entropy/WitnessList.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.SharpRamseyFive.ResidualCertificate.exists_witness_list line 20
  2. theorem OAI.SharpRamseyFive.ResidualCertificate.exists_residual_roots line 30
  3. def OAI.SharpRamseyFive.ResidualCertificate.sharedBatches line 70
  4. def OAI.SharpRamseyFive.ResidualCertificate.touchedBatches line 73
  5. theorem OAI.SharpRamseyFive.ResidualCertificate.roots_from_shared_hits line 78
  6. def OAI.SharpRamseyFive.ResidualCertificate.encodedDirections line 152
  7. def OAI.SharpRamseyFive.ResidualCertificate.touchedToEncoded line 155
  8. def OAI.SharpRamseyFive.ResidualCertificate.batchesOn line 159
  9. def OAI.SharpRamseyFive.ResidualCertificate.survivingDirections line 162
  10. lemma OAI.SharpRamseyFive.ResidualCertificate.mem_batchesOn line 166
  11. lemma OAI.SharpRamseyFive.ResidualCertificate.surviving_touches line 172
  12. lemma OAI.SharpRamseyFive.ResidualCertificate.batchesOn_card_le line 198
  13. lemma OAI.SharpRamseyFive.ResidualCertificate.surviving_touches_card line 209
  14. lemma OAI.SharpRamseyFive.ResidualCertificate.terminal_high_loss line 225
  15. lemma OAI.SharpRamseyFive.ResidualCertificate.terminal_low_loss line 234
  16. theorem OAI.SharpRamseyFive.ResidualCertificate.terminal_state_roots line 241
  17. def OAI.SharpRamseyFive.ResidualCertificate.outsideDirections line 266
  18. inductive OAI.SharpRamseyFive.ResidualCertificate.EncodingStep line 269
  19. lemma OAI.SharpRamseyFive.ResidualCertificate.encodingStep_strict line 279
  20. lemma OAI.SharpRamseyFive.ResidualCertificate.encoding_reachable_subset line 287
  21. theorem OAI.SharpRamseyFive.ResidualCertificate.exists_terminal_encoding line 296
  22. theorem OAI.SharpRamseyFive.ResidualCertificate.high_case_certificate_geometry line 322
  23. theorem OAI.SharpRamseyFive.ResidualCertificate.low_case_certificate_geometry line 352
  24. def OAI.SharpRamseyFive.ResidualCertificate.paidDirections line 382
  25. def OAI.SharpRamseyFive.ResidualCertificate.Realized line 384
  26. def OAI.SharpRamseyFive.ResidualCertificate.DictionaryInvariant line 387
  27. lemma OAI.SharpRamseyFive.ResidualCertificate.encodedDirections_mono line 391
  28. lemma OAI.SharpRamseyFive.ResidualCertificate.paidDirections_union line 398
  29. lemma OAI.SharpRamseyFive.ResidualCertificate.realized_union line 403
  30. def OAI.SharpRamseyFive.ResidualCertificate.anchorEvents line 410
  31. lemma OAI.SharpRamseyFive.ResidualCertificate.anchorEvents_fresh line 415
  32. lemma OAI.SharpRamseyFive.ResidualCertificate.anchorEvents_card line 425
  33. lemma OAI.SharpRamseyFive.ResidualCertificate.anchorEvents_directions line 430