OAI/Probability/ThorpCompatibility/LightRescaling.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThorpCompatibility.Law.prob line 13
  2. lemma OAI.ThorpCompatibility.Law.prob_nonneg line 16
  3. lemma OAI.ThorpCompatibility.Law.prob_le_one line 19
  4. lemma OAI.ThorpCompatibility.Law.prob_mono line 23
  5. lemma OAI.ThorpCompatibility.Law.mass_le_prob line 32
  6. lemma OAI.ThorpCompatibility.Law.prob_not line 39
  7. lemma OAI.ThorpCompatibility.Law.prob_eq_mean line 47
  8. def OAI.ThorpCompatibility.Law.lightRescale line 54
  9. lemma OAI.ThorpCompatibility.Law.lightRescale_mass_of_not line 79
  10. lemma OAI.ThorpCompatibility.Law.lightRescale_mass_of_mem line 84
  11. lemma OAI.ThorpCompatibility.Law.lightRescale_pos line 91
  12. lemma OAI.ThorpCompatibility.Law.lightRescale_log line 99
  13. lemma OAI.ThorpCompatibility.Law.light_cost_nonneg line 113
  14. lemma OAI.ThorpCompatibility.Law.condEntropy_light_comparison line 122