OAI/Combinatorics/SharpRamsey/Exposure/ExposureBudget.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

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

  1. structure OAI.SharpLogRamsey.Selection.Law line 14
  2. def OAI.SharpLogRamsey.Selection.entropy line 21
  3. theorem OAI.SharpLogRamsey.Selection.entropy_ge_neg_log line 23
  4. def OAI.SharpLogRamsey.Selection.Law.map line 36
  5. theorem OAI.SharpLogRamsey.Selection.card_fixed_coordinates line 42
  6. abbrev OAI.SharpLogRamsey.Selection.Positions line 64
  7. def OAI.SharpLogRamsey.Selection.positionMap line 66
  8. def OAI.SharpLogRamsey.Selection.Occurs line 69
  9. theorem OAI.SharpLogRamsey.Selection.card_occurs line 72
  10. theorem OAI.SharpLogRamsey.Selection.card_occurs_two line 89
  11. def OAI.SharpLogRamsey.Selection.Law.fst line 101
  12. def OAI.SharpLogRamsey.Selection.Law.snd line 106
  13. theorem OAI.SharpLogRamsey.Selection.selected_atom_bound line 111
  14. theorem OAI.SharpLogRamsey.Selection.selected_entropy_bound line 152
  15. def OAI.SharpLogRamsey.Selection.Law.AbsolutelyContinuous line 172
  16. def OAI.SharpLogRamsey.Selection.divergence line 174
  17. theorem OAI.SharpLogRamsey.Selection.Law.mass_le_one line 177
  18. theorem OAI.SharpLogRamsey.Selection.entropy_nonneg line 181
  19. theorem OAI.SharpLogRamsey.Selection.mul_log_div_ge line 186
  20. theorem OAI.SharpLogRamsey.Selection.divergence_nonneg line 199
  21. def OAI.SharpLogRamsey.Selection.Law.event line 205
  22. theorem OAI.SharpLogRamsey.Selection.Law.event_nonneg line 207
  23. theorem OAI.SharpLogRamsey.Selection.Law.event_le_one line 210
  24. theorem OAI.SharpLogRamsey.Selection.event_transfer line 214
  25. def OAI.SharpLogRamsey.Selection.Law.prod line 242
  26. theorem OAI.SharpLogRamsey.Selection.Law.le_fst line 247
  27. theorem OAI.SharpLogRamsey.Selection.Law.le_snd line 250
  28. theorem OAI.SharpLogRamsey.Selection.Law.absContinuous_prod line 253
  29. def OAI.SharpLogRamsey.Selection.mutualInfo line 259
  30. theorem OAI.SharpLogRamsey.Selection.mutualInfo_eq_divergence line 262
  31. theorem OAI.SharpLogRamsey.Selection.mutualInfo_nonneg line 288
  32. theorem OAI.SharpLogRamsey.Selection.entropy_subadditive line 292
  33. theorem OAI.SharpLogRamsey.Selection.mutualInfo_event_transfer line 297
  34. theorem OAI.SharpLogRamsey.Selection.Law.sum_map line 307
  35. theorem OAI.SharpLogRamsey.Selection.entropy_map line 318
  36. theorem OAI.SharpLogRamsey.Selection.Law.le_map line 322
  37. theorem OAI.SharpLogRamsey.Selection.entropy_map_le line 327
  38. def OAI.SharpLogRamsey.Selection.Law.condFst line 337
  39. theorem OAI.SharpLogRamsey.Selection.Law.condFst_mass line 346
  40. theorem OAI.SharpLogRamsey.Selection.Law.snd_mul_condFst line 350
  41. theorem OAI.SharpLogRamsey.Selection.entropy_chain line 358
  42. theorem OAI.SharpLogRamsey.Selection.conditional_entropy_le line 381
  43. theorem OAI.SharpLogRamsey.Selection.log_sum line 387