OAI/Analysis/PlanarEndpoint/Information/FiniteTables.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Finite information laws, entropy and convergence of probability measures.

  1. def OAI.PlanarEndpoint.TransverseInformation.rowMass line 15
  2. def OAI.PlanarEndpoint.TransverseInformation.colMass line 16
  3. def OAI.PlanarEndpoint.TransverseInformation.conditionalMass line 17
  4. lemma OAI.PlanarEndpoint.TransverseInformation.rowMass_nonneg line 21
  5. lemma OAI.PlanarEndpoint.TransverseInformation.colMass_nonneg line 25
  6. lemma OAI.PlanarEndpoint.TransverseInformation.le_rowMass line 29
  7. lemma OAI.PlanarEndpoint.TransverseInformation.le_colMass line 33
  8. lemma OAI.PlanarEndpoint.TransverseInformation.conditional_information_chain line 36
  9. lemma OAI.PlanarEndpoint.TransverseInformation.joint_information_chain line 43
  10. lemma OAI.PlanarEndpoint.TransverseInformation.joint_conditioning_exception_le line 49
  11. lemma OAI.PlanarEndpoint.TransverseInformation.information_gt_iff line 85
  12. lemma OAI.PlanarEndpoint.TransverseInformation.conditional_determination_exception_le line 101
  13. lemma OAI.PlanarEndpoint.TransverseInformation.sub_le_mul_log_div line 131
  14. lemma OAI.PlanarEndpoint.TransverseInformation.information_nonneg line 145
  15. lemma OAI.PlanarEndpoint.TransverseInformation.expected_conditioning_decrement_nonneg line 151
  16. def OAI.PlanarEndpoint.TransverseInformation.entropy line 191
  17. def OAI.PlanarEndpoint.TransverseInformation.conditionalEntropy line 193
  18. lemma OAI.PlanarEndpoint.TransverseInformation.expected_conditioning_decrement_eq line 196
  19. lemma OAI.PlanarEndpoint.TransverseInformation.entropy_conditioning_le line 206
  20. lemma OAI.PlanarEndpoint.TransverseInformation.conditionalEntropy_nonneg line 214
  21. lemma OAI.PlanarEndpoint.TransverseInformation.entropy_nonneg line 229
  22. lemma OAI.PlanarEndpoint.TransverseInformation.entropy_joint_eq line 237
  23. lemma OAI.PlanarEndpoint.TransverseInformation.entropy_joint_swap line 257
  24. lemma OAI.PlanarEndpoint.TransverseInformation.conditioning_decrement_le_label_entropy line 263
  25. lemma OAI.PlanarEndpoint.TransverseInformation.entropy_le_log_card line 274
  26. lemma OAI.PlanarEndpoint.TransverseInformation.direction_bin_cost_bound line 311