OAI/Probability/GaussianInformation/Dyadic/Entropy.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RepeatedLocalization.xlog line 18
  2. lemma OAI.RepeatedLocalization.continuous_xlog line 20
  3. lemma OAI.RepeatedLocalization.xlog_zero line 21
  4. lemma OAI.RepeatedLocalization.xlog_one line 22
  5. lemma OAI.RepeatedLocalization.xlog_mul line 23
  6. lemma OAI.RepeatedLocalization.mul_log_div_le line 29
  7. lemma OAI.RepeatedLocalization.xlog_lower_tangent line 37
  8. lemma OAI.RepeatedLocalization.integrable_bounded_measurable line 49
  9. lemma OAI.RepeatedLocalization.integrable_xlog_probability line 55
  10. def OAI.RepeatedLocalization.scoreMass line 65
  11. def OAI.RepeatedLocalization.infoContribution line 68
  12. lemma OAI.RepeatedLocalization.scoreMass_nonneg line 72
  13. lemma OAI.RepeatedLocalization.scoreMass_le_one line 76
  14. lemma OAI.RepeatedLocalization.infoContribution_zero_mass line 82
  15. lemma OAI.RepeatedLocalization.infoContribution_nonneg line 91
  16. lemma OAI.RepeatedLocalization.xlog_upper_quadratic line 114
  17. lemma OAI.RepeatedLocalization.infoContribution_le_log_l2bound line 123
  18. lemma OAI.RepeatedLocalization.log_ratio_lower line 159
  19. lemma OAI.RepeatedLocalization.finite_log_sum line 171
  20. lemma OAI.RepeatedLocalization.log_ratio_mul line 185
  21. lemma OAI.RepeatedLocalization.neg_xlog_le_one line 192
  22. lemma OAI.RepeatedLocalization.xlog_nonpos line 197
  23. lemma OAI.RepeatedLocalization.finite_entropy_mass_bound line 200