OAI/Combinatorics/SharpRamsey/Marking/TargetEvent.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

High-rank geometric supports and entropy estimates.

  1. lemma OAI.SharpLogRamsey.HighRankExcess.target_event_eq line 19
  2. lemma OAI.SharpLogRamsey.HighRankExcess.target_excess_mass_sharp line 41
  3. def OAI.SharpLogRamsey.ProductLaw.weight line 65
  4. lemma OAI.SharpLogRamsey.ProductLaw.total line 68
  5. lemma OAI.SharpLogRamsey.ProductLaw.nonneg line 74
  6. lemma OAI.SharpLogRamsey.ProductLaw.reindex line 77
  7. lemma OAI.SharpLogRamsey.ProductLaw.restriction line 90
  8. lemma OAI.SharpLogRamsey.ProductLaw.marginal line 128
  9. lemma OAI.SharpLogRamsey.ProductLaw.coordinate_mean line 141
  10. lemma OAI.SharpLogRamsey.ProductLaw.row_exists_le line 158
  11. def OAI.SharpLogRamsey.FiniteMarginals.marginal line 194
  12. lemma OAI.SharpLogRamsey.FiniteMarginals.sum_marginal line 197
  13. lemma OAI.SharpLogRamsey.FiniteMarginals.marginal_total line 207
  14. lemma OAI.SharpLogRamsey.FiniteMarginals.marginal_nonneg line 211
  15. lemma OAI.SharpLogRamsey.FiniteMarginals.row_mass line 220
  16. lemma OAI.SharpLogRamsey.FiniteMarginals.row_pushforward line 237
  17. def OAI.SharpLogRamsey.HighRankSize.rankPoints line 259
  18. def OAI.SharpLogRamsey.HighRankSize.points line 263
  19. def OAI.SharpLogRamsey.HighRankSize.domain line 268
  20. lemma OAI.SharpLogRamsey.HighRankSize.partner_bound line 274
  21. lemma OAI.SharpLogRamsey.HighRankSize.domain_card line 284
  22. lemma OAI.SharpLogRamsey.HighRankSize.mean_points line 314
  23. theorem OAI.SharpLogRamsey.HighRankSize.expected_domain line 340
  24. def OAI.SharpLogRamsey.FiniteRowProcess.weight line 376
  25. lemma OAI.SharpLogRamsey.FiniteRowProcess.weight_nonneg line 379
  26. lemma OAI.SharpLogRamsey.FiniteRowProcess.weight_total line 382
  27. def OAI.SharpLogRamsey.FiniteRowProcess.run line 388
  28. def OAI.SharpLogRamsey.FiniteRowProcess.expected line 392
  29. lemma OAI.SharpLogRamsey.FiniteRowProcess.expected_zero line 395
  30. lemma OAI.SharpLogRamsey.FiniteRowProcess.expected_succ line 398
  31. lemma OAI.SharpLogRamsey.FiniteRowProcess.expected_le_one line 408
  32. lemma OAI.SharpLogRamsey.FiniteRowProcess.rank_run line 417
  33. theorem OAI.SharpLogRamsey.FiniteRowProcess.rank_reached line 424