OAI/Probability/ThorpCompatibility/Entropy.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpCompatibility.Law.ext line 12
  2. lemma OAI.ThorpCompatibility.Law.mean_const line 18
  3. lemma OAI.ThorpCompatibility.Law.mean_add line 21
  4. lemma OAI.ThorpCompatibility.Law.mean_sub line 25
  5. lemma OAI.ThorpCompatibility.Law.mean_mul_const line 29
  6. lemma OAI.ThorpCompatibility.Law.mean_const_mul line 33
  7. lemma OAI.ThorpCompatibility.Law.mean_mono line 37
  8. lemma OAI.ThorpCompatibility.Law.mean_congr_support line 41
  9. lemma OAI.ThorpCompatibility.Law.map_mass_mean line 49
  10. lemma OAI.ThorpCompatibility.Law.map_map line 54
  11. lemma OAI.ThorpCompatibility.Law.map_id line 61
  12. lemma OAI.ThorpCompatibility.Law.mass_le_one line 66
  13. lemma OAI.ThorpCompatibility.Law.mass_le_map line 70
  14. lemma OAI.ThorpCompatibility.Law.map_mass_pos line 78
  15. def OAI.ThorpCompatibility.Law.entropy line 81
  16. lemma OAI.ThorpCompatibility.Law.uniformDeficit_eq line 83
  17. lemma OAI.ThorpCompatibility.Law.entropy_nonneg line 87
  18. lemma OAI.ThorpCompatibility.Law.entropy_map_injective line 95
  19. def OAI.ThorpCompatibility.Law.condMass line 104
  20. def OAI.ThorpCompatibility.Law.condEntropy line 108
  21. lemma OAI.ThorpCompatibility.Law.condMass_pos line 111
  22. lemma OAI.ThorpCompatibility.Law.condEntropy_eq_mean line 115
  23. lemma OAI.ThorpCompatibility.Law.entropy_pair_comm line 129
  24. lemma OAI.ThorpCompatibility.Law.entropy_func_pair line 136
  25. lemma OAI.ThorpCompatibility.Law.condEntropy_const line 141