OAI/Combinatorics/SharpRamsey/Exposure/DivergenceMap.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.SharpLogRamsey.Selection.divergence_map_le line 14
  2. theorem OAI.SharpLogRamsey.Selection.Law.ext line 30
  3. theorem OAI.SharpLogRamsey.Selection.Law.map_id line 37
  4. theorem OAI.SharpLogRamsey.Selection.Law.map_map line 41
  5. theorem OAI.SharpLogRamsey.Selection.Law.map_fst line 48
  6. theorem OAI.SharpLogRamsey.Selection.Law.map_snd line 54
  7. theorem OAI.SharpLogRamsey.Selection.Law.prod_map line 58
  8. theorem OAI.SharpLogRamsey.Selection.Law.fst_map_pair line 70
  9. theorem OAI.SharpLogRamsey.Selection.Law.snd_map_pair line 75
  10. theorem OAI.SharpLogRamsey.Selection.mutualInfo_map_le line 80
  11. theorem OAI.SharpLogRamsey.Selection.entropy_map_eq_of_leftInverse line 86
  12. theorem OAI.SharpLogRamsey.Selection.entropy_pair_self line 93
  13. theorem OAI.SharpLogRamsey.Selection.Law.fst_map_self line 97
  14. theorem OAI.SharpLogRamsey.Selection.Law.snd_map_self line 102
  15. def OAI.SharpLogRamsey.Selection.Law.cond line 107
  16. theorem OAI.SharpLogRamsey.Selection.Law.cond_mass line 110
  17. theorem OAI.SharpLogRamsey.Selection.Law.cond_map_weight line 119
  18. theorem OAI.SharpLogRamsey.Selection.entropy_cond_chain line 137
  19. theorem OAI.SharpLogRamsey.Selection.entropy_cond_self line 155
  20. def OAI.SharpLogRamsey.Selection.Law.pi line 165
  21. def OAI.SharpLogRamsey.Selection.Law.marginal line 172
  22. def OAI.SharpLogRamsey.Selection.totalCorrelation line 175
  23. theorem OAI.SharpLogRamsey.Selection.Law.absContinuous_pi line 178
  24. theorem OAI.SharpLogRamsey.Selection.totalCorrelation_eq_divergence line 186
  25. theorem OAI.SharpLogRamsey.Selection.totalCorrelation_nonneg line 211
  26. theorem OAI.SharpLogRamsey.Selection.entropy_subadditive_pi line 215
  27. theorem OAI.SharpLogRamsey.Selection.Law.map_mass_injective line 221
  28. theorem OAI.SharpLogRamsey.Selection.entropy_map_eq_of_injective line 227
  29. def OAI.SharpLogRamsey.Selection.Law.restrict line 233
  30. theorem OAI.SharpLogRamsey.Selection.entropy_restrict_chain line 236
  31. theorem OAI.SharpLogRamsey.Selection.entropy_marginal_cond line 249
  32. theorem OAI.SharpLogRamsey.Selection.Law.marginal_restrict line 263
  33. theorem OAI.SharpLogRamsey.Selection.totalCorrelation_drop line 269
  34. theorem OAI.SharpLogRamsey.Selection.fresh_draw_identity line 299
  35. def OAI.SharpLogRamsey.Selection.pairInformation line 335
  36. def OAI.SharpLogRamsey.Selection.exposedInformation line 338
  37. def OAI.SharpLogRamsey.Selection.maximumInformation line 341
  38. lemma OAI.SharpLogRamsey.Selection.pairInformation_le_exposed line 344
  39. lemma OAI.SharpLogRamsey.Selection.maximumInformation_le_exposed line 352
  40. theorem OAI.SharpLogRamsey.Selection.maximum_exposure_drop line 358
  41. def OAI.SharpLogRamsey.Selection.freshRepresentatives line 381
  42. def OAI.SharpLogRamsey.Selection.otherRepresentatives line 384
  43. lemma OAI.SharpLogRamsey.Selection.otherRepresentatives_sub line 389
  44. lemma OAI.SharpLogRamsey.Selection.otherRepresentatives_update line 394
  45. theorem OAI.SharpLogRamsey.Selection.selected_maximum_absorption line 405
  46. theorem OAI.SharpLogRamsey.Selection.fresh_round_drop line 435