OAI/Probability/ThorpCompatibility/FiniteLaw.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ThorpCompatibility.Law line 10
  2. def OAI.ThorpCompatibility.Law.mean line 18
  3. def OAI.ThorpCompatibility.Law.relativeEntropy line 20
  4. def OAI.ThorpCompatibility.Law.uniformDeficit line 23
  5. def OAI.ThorpCompatibility.Law.uniform line 26
  6. def OAI.ThorpCompatibility.Law.map line 31
  7. lemma OAI.ThorpCompatibility.Law.mean_map line 42
  8. lemma OAI.ThorpCompatibility.Law.pointwise_entropy_lower line 51
  9. lemma OAI.ThorpCompatibility.Law.relativeEntropy_nonneg line 62
  10. lemma OAI.ThorpCompatibility.Law.relativeEntropy_uniform line 69
  11. lemma OAI.ThorpCompatibility.Law.uniformDeficit_nonneg line 84
  12. def OAI.ThorpCompatibility.Law.tilt line 92
  13. lemma OAI.ThorpCompatibility.Law.gibbs_le line 98
  14. lemma OAI.ThorpCompatibility.Law.entropy_moment_bound line 121