OAI/Combinatorics/SharpRamsey/Exposure/RemainingEmbedding.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Entropy and counting bounds for selected coordinates in finite probability laws.

  1. def OAI.SharpLogRamsey.Selection.remainingEmbedding line 17
  2. lemma OAI.SharpLogRamsey.Selection.remaining_own line 38
  3. def OAI.SharpLogRamsey.Selection.roundInformation line 42
  4. def OAI.SharpLogRamsey.Selection.nextPotential line 46
  5. lemma OAI.SharpLogRamsey.Selection.roundInformation_nonneg line 51
  6. lemma OAI.SharpLogRamsey.Selection.nextPotential_nonneg line 56
  7. theorem OAI.SharpLogRamsey.Selection.roundInformation_budget line 62
  8. def OAI.SharpLogRamsey.Selection.exposureScores line 95
  9. lemma OAI.SharpLogRamsey.Selection.exposureScores_zero line 107
  10. lemma OAI.SharpLogRamsey.Selection.exposureScores_succ line 111
  11. theorem OAI.SharpLogRamsey.Selection.exposureScores_sum_le line 122
  12. theorem OAI.SharpLogRamsey.Selection.exists_exposure_round line 162
  13. def OAI.SharpLogRamsey.Selection.tupleDeficit line 185
  14. lemma OAI.SharpLogRamsey.Selection.marginal_deficit_sum line 188
  15. lemma OAI.SharpLogRamsey.Selection.tupleDeficit_nonneg line 194
  16. theorem OAI.SharpLogRamsey.Selection.tupleDeficit_drop line 198
  17. lemma OAI.SharpLogRamsey.Selection.tupleDeficit_expected_le line 210
  18. theorem OAI.SharpLogRamsey.Selection.tupleDeficit_restrict_le line 219
  19. lemma OAI.SharpLogRamsey.Selection.totalCorrelation_le_tupleDeficit line 242
  20. theorem OAI.SharpLogRamsey.Selection.entropy_le_log_card line 253
  21. lemma OAI.SharpLogRamsey.Selection.Law.map_support line 290
  22. lemma OAI.SharpLogRamsey.Selection.Law.cond_support line 301
  23. lemma OAI.SharpLogRamsey.Selection.entropy_mapped_support line 309
  24. def OAI.SharpLogRamsey.Selection.tupleSupported line 324
  25. lemma OAI.SharpLogRamsey.Selection.tupleSupported_marginal_cap line 327
  26. lemma OAI.SharpLogRamsey.Selection.tupleSupported_cond_restrict line 332
  27. def OAI.SharpLogRamsey.Selection.exposureDeficits line 349
  28. lemma OAI.SharpLogRamsey.Selection.exposureDeficits_zero line 361
  29. lemma OAI.SharpLogRamsey.Selection.exposureDeficits_succ line 365
  30. theorem OAI.SharpLogRamsey.Selection.exposureDeficits_le line 375