OAI/Combinatorics/SharpRamsey/Entropy/MakePair.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.SharpRamseyFive.CertificateCover.make_pair line 27
  2. lemma OAI.SharpRamseyFive.CertificateCover.make_root line 69
  3. abbrev OAI.SharpRamseyFive.CertificateCover.Word line 86
  4. abbrev OAI.SharpRamseyFive.CertificateCover.finish line 87
  5. abbrev OAI.SharpRamseyFive.CertificateCover.charge line 89
  6. def OAI.SharpRamseyFive.CertificateCover.degreeSum line 92
  7. def OAI.SharpRamseyFive.CertificateCover.TraceOK line 96
  8. def OAI.SharpRamseyFive.CertificateCover.append line 102
  9. lemma OAI.SharpRamseyFive.CertificateCover.finish_append line 108
  10. lemma OAI.SharpRamseyFive.CertificateCover.degreeSum_append line 116
  11. lemma OAI.SharpRamseyFive.CertificateCover.charge_append line 127
  12. lemma OAI.SharpRamseyFive.CertificateCover.traceOK_append line 138
  13. lemma OAI.SharpRamseyFive.CertificateCover.one_le_degree line 147
  14. lemma OAI.SharpRamseyFive.CertificateCover.length_le_degreeSum line 158
  15. lemma OAI.SharpRamseyFive.CertificateCover.trace_weight line 170
  16. def OAI.SharpRamseyFive.CertificateCover.Segment line 185
  17. lemma OAI.SharpRamseyFive.CertificateCover.segment_empty line 191
  18. lemma OAI.SharpRamseyFive.CertificateCover.segment_single line 197
  19. lemma OAI.SharpRamseyFive.CertificateCover.segment_append line 207
  20. lemma OAI.SharpRamseyFive.CertificateCover.make_encoding line 220
  21. theorem OAI.SharpRamseyFive.CertificateCover.encoding_path_program line 243
  22. lemma OAI.SharpRamseyFive.CertificateCover.encode_set line 265
  23. lemma OAI.SharpRamseyFive.CertificateCover.residual_program line 302
  24. theorem OAI.SharpRamseyFive.CertificateCover.bad_program_high line 373
  25. theorem OAI.SharpRamseyFive.CertificateCover.bad_program_low line 404
  26. lemma OAI.SharpRamseyFive.CertificateCover.decoded_static_union_bound line 426
  27. abbrev OAI.SharpRamseyFive.CertificateCover.AllPrograms line 451
  28. def OAI.SharpRamseyFive.CertificateCover.CompleteProgram line 454
  29. def OAI.SharpRamseyFive.CertificateCover.completePrograms line 459
  30. instance OAI.SharpRamseyFive.CertificateCover.completePrograms_fintype line 462