OAI/Combinatorics/SharpRamsey/Entropy/SinglesUnique.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.ComponentPartition.singles_iff_unique line 21
  2. lemma OAI.SharpRamseyFive.ComponentPartition.large_card_sum line 38
  3. def OAI.SharpRamseyFive.ComponentPartition.componentMap line 44
  4. lemma OAI.SharpRamseyFive.ComponentPartition.componentMap_eq_iff line 47
  5. lemma OAI.SharpRamseyFive.ComponentPartition.componentMap_idempotent line 58
  6. lemma OAI.SharpRamseyFive.ComponentEnumeration.boundary_of_walk line 70
  7. lemma OAI.SharpRamseyFive.ComponentEnumeration.connected_boundary line 80
  8. def OAI.SharpRamseyFive.ComponentEnumeration.relationGraph line 96
  9. abbrev OAI.SharpRamseyFive.ComponentEnumeration.Extension line 101
  10. def OAI.SharpRamseyFive.ComponentEnumeration.extend line 102
  11. lemma OAI.SharpRamseyFive.ComponentEnumeration.extension_card line 106
  12. lemma OAI.SharpRamseyFive.ComponentEnumeration.dword_card_le line 119
  13. theorem OAI.SharpRamseyFive.ComponentEnumeration.connected_extension_cover line 137
  14. abbrev OAI.SharpRamseyFive.ComponentEnumeration.RelatedPair line 175
  15. abbrev OAI.SharpRamseyFive.ComponentEnumeration.Seed line 176
  16. def OAI.SharpRamseyFive.ComponentEnumeration.seedStart line 177
  17. theorem OAI.SharpRamseyFive.ComponentEnumeration.connected_tuple_count line 180
  18. lemma OAI.SharpRamseyFive.ComponentPartition.connected_fiber line 247
  19. def OAI.SharpRamseyFive.ComponentPartition.connectedWeight line 270
  20. lemma OAI.SharpRamseyFive.ComponentPartition.connectedWeight_nonneg line 275
  21. lemma OAI.SharpRamseyFive.ComponentPartition.connectedWeight_sum_le line 281
  22. lemma OAI.SharpRamseyFive.ComponentPartition.univ_sub_large line 304
  23. lemma OAI.SharpRamseyFive.ComponentPartition.partition_block_bound line 309
  24. theorem OAI.SharpRamseyFive.ComponentPartition.graph_partition_sum line 336
  25. def OAI.SharpRamseyFive.AmbientEnumeration.overlapRelation line 398
  26. lemma OAI.SharpRamseyFive.AmbientEnumeration.overlapRelation_symm line 402
  27. lemma OAI.SharpRamseyFive.AmbientEnumeration.relation_graph_eq line 410
  28. lemma OAI.SharpRamseyFive.AmbientEnumeration.simple_image line 416
  29. lemma OAI.SharpRamseyFive.AmbientEnumeration.simple_card line 430
  30. lemma OAI.SharpRamseyFive.AmbientEnumeration.large_image line 435