OAI/Combinatorics/RamseyFive/Entropy/Rectangle.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SharpRamseyFive.CoreGeometry.count_subspaces line 13
  2. theorem OAI.SharpRamseyFive.CoreGeometry.card_rectangle line 39
  3. theorem OAI.SharpRamseyFive.CoreGeometry.card_rectangle_le line 56
  4. lemma OAI.SharpRamseyFive.FiniteEntropy.exp_single_hit line 86
  5. theorem OAI.SharpRamseyFive.FiniteEntropy.exp_hits line 98
  6. theorem OAI.SharpRamseyFive.FiniteEntropy.exp_hits_le line 114
  7. theorem OAI.SharpRamseyFive.FiniteEntropy.iid_occupancy_tail line 128
  8. lemma OAI.SharpRamseyFive.FiniteEntropy.event_biUnion_le line 143
  9. theorem OAI.SharpRamseyFive.FiniteEntropy.all_occupancy_tail line 159
  10. def OAI.SharpRamseyFive.FiniteEntropy.uniform line 182
  11. lemma OAI.SharpRamseyFive.FiniteEntropy.uniform_event line 190
  12. abbrev OAI.SharpRamseyFive.RectangleGeometry.Flag line 202
  13. theorem OAI.SharpRamseyFive.RectangleGeometry.card_flags line 204
  14. theorem OAI.SharpRamseyFive.RectangleGeometry.card_flags_lower line 217
  15. lemma OAI.SharpRamseyFive.RectangleGeometry.flags_nonempty line 227
  16. def OAI.SharpRamseyFive.RectangleGeometry.rectangle line 231
  17. lemma OAI.SharpRamseyFive.RectangleGeometry.card_rectangle_flags line 235
  18. theorem OAI.SharpRamseyFive.RectangleGeometry.rectangle_mass line 252
  19. lemma OAI.SharpRamseyFive.RectangleGeometry.count_rectangles line 275
  20. lemma OAI.SharpRamseyFive.RectangleGeometry.rectangle_tail_scalar line 292
  21. lemma OAI.SharpRamseyFive.RectangleGeometry.rectangle_mean line 302
  22. theorem OAI.SharpRamseyFive.RectangleGeometry.rectangle_occupancy_tail line 316