OAI/Combinatorics/SharpRamsey/Entropy/LabelledFilterCard.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.SharpRamseyFive.SelectionBridge.labelled_filter_card line 26
  2. lemma OAI.SharpRamseyFive.SelectionBridge.vertexBadMass_nonneg line 36
  3. theorem OAI.SharpRamseyFive.SelectionBridge.all_bad_residual_sum_le line 41
  4. def OAI.SharpRamseyFive.ResidualElimination.Agrees line 95
  5. def OAI.SharpRamseyFive.ResidualElimination.completionSum line 97
  6. lemma OAI.SharpRamseyFive.ResidualElimination.completionSum_nonneg line 101
  7. lemma OAI.SharpRamseyFive.ResidualElimination.completionSum_mono line 110
  8. lemma OAI.SharpRamseyFive.ResidualElimination.completionSum_congr line 120
  9. lemma OAI.SharpRamseyFive.ResidualElimination.completionSum_mul line 128
  10. lemma OAI.SharpRamseyFive.ResidualElimination.completionSum_sum line 133
  11. lemma OAI.SharpRamseyFive.ResidualElimination.agrees_erase_iff line 144
  12. lemma OAI.SharpRamseyFive.ResidualElimination.completionSum_expose line 159
  13. lemma OAI.SharpRamseyFive.ResidualElimination.completionSum_empty line 171
  14. def OAI.SharpRamseyFive.ResidualElimination.term line 182
  15. lemma OAI.SharpRamseyFive.ResidualElimination.term_nonneg line 186
  16. lemma OAI.SharpRamseyFive.ResidualElimination.prod_erase_le line 192
  17. lemma OAI.SharpRamseyFive.ResidualElimination.erase_sdiff line 200
  18. lemma OAI.SharpRamseyFive.ResidualElimination.double_erase_sdiff line 206
  19. lemma OAI.SharpRamseyFive.ResidualElimination.term_shift_step line 212
  20. lemma OAI.SharpRamseyFive.ResidualElimination.sum_known_partner line 240
  21. lemma OAI.SharpRamseyFive.ResidualElimination.sum_new_partner line 267
  22. theorem OAI.SharpRamseyFive.ResidualElimination.shift_bad_enumeration line 302
  23. lemma OAI.SharpRamseyFive.SingletonEnumeration.vertexBadMass_antitone line 395
  24. lemma OAI.SharpRamseyFive.SingletonEnumeration.sum_powers_le line 408
  25. lemma OAI.SharpRamseyFive.SingletonEnumeration.actual_bad_completion line 422
  26. def OAI.SharpRamseyFive.SingletonEnumeration.shiftKernel line 455
  27. lemma OAI.SharpRamseyFive.SingletonEnumeration.shiftKernel_range line 460