OAI/Combinatorics/SharpRamsey/Entropy/PatchNotMem.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.SharpRamseyFive.ResidualElimination.patch_notMem line 21
  2. lemma OAI.SharpRamseyFive.ResidualElimination.agrees_sdiff_patch line 25
  3. lemma OAI.SharpRamseyFive.ResidualElimination.completionSum_split line 42
  4. theorem OAI.SharpRamseyFive.ResidualElimination.weighted_block_exposure line 52
  5. theorem OAI.SharpRamseyFive.ResidualElimination.independent_positions_exposure line 69
  6. lemma OAI.SharpRamseyFive.ResidualElimination.powerset_sdiff line 96
  7. lemma OAI.SharpRamseyFive.ResidualElimination.sum_disjoint_swap line 109
  8. def OAI.SharpRamseyFive.ResidualElimination.badExpansion line 120
  9. lemma OAI.SharpRamseyFive.ResidualElimination.badExpansion_nonneg line 125
  10. lemma OAI.SharpRamseyFive.ResidualElimination.badExpansion_add line 135
  11. lemma OAI.SharpRamseyFive.ResidualElimination.badExpansion_sum_le line 151
  12. theorem OAI.SharpRamseyFive.ResidualElimination.all_singleton_enumeration line 170
  13. def OAI.SharpRamseyFive.SingletonEnumeration.independentWeight line 225
  14. lemma OAI.SharpRamseyFive.SingletonEnumeration.independentWeight_nonneg line 231
  15. theorem OAI.SharpRamseyFive.SingletonEnumeration.actual_all_singleton_enumeration line 236
  16. lemma OAI.SharpRamseyFive.SingletonEnumeration.inside_sum_le line 300
  17. lemma OAI.SharpRamseyFive.SingletonEnumeration.extraWeight_le_independent line 312
  18. theorem OAI.SharpRamseyFive.SingletonEnumeration.designation_sum_le_vertex line 328
  19. theorem OAI.SharpRamseyFive.ResidualElimination.disjoint_blocks_exposure line 362
  20. def OAI.SharpRamseyFive.ComponentPartition.fiber line 411
  21. def OAI.SharpRamseyFive.ComponentPartition.singles line 413
  22. def OAI.SharpRamseyFive.ComponentPartition.largeLabels line 415
  23. lemma OAI.SharpRamseyFive.ComponentPartition.mem_fiber line 419
  24. lemma OAI.SharpRamseyFive.ComponentPartition.mem_singles line 422
  25. lemma OAI.SharpRamseyFive.ComponentPartition.mem_largeLabels line 425
  26. lemma OAI.SharpRamseyFive.ComponentPartition.self_mem_fiber line 429
  27. lemma OAI.SharpRamseyFive.ComponentPartition.fiber_card_pos line 431
  28. lemma OAI.SharpRamseyFive.ComponentPartition.fiber_disjoint line 435
  29. lemma OAI.SharpRamseyFive.ComponentPartition.large_union line 441