OAI/Probability/Ballisticity/Entropy/EntropyVariational.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DirectionalTransience.Entropy.entropy_test_le line 14
  2. theorem OAI.DirectionalTransience.Entropy.entropy_exp_test_le line 30
  3. lemma OAI.DirectionalTransience.Entropy.entropy_young_exact line 41
  4. def OAI.DirectionalTransience.Entropy.ExpBudget line 54
  5. lemma OAI.DirectionalTransience.Entropy.integrable_of_bounded line 58
  6. lemma OAI.DirectionalTransience.Entropy.exp_integrable_of_bounded line 64
  7. lemma OAI.DirectionalTransience.Entropy.expBudget_of_kl_le line 73
  8. lemma OAI.DirectionalTransience.Entropy.ExpBudget.nonneg line 81
  9. lemma OAI.DirectionalTransience.Entropy.ExpBudget.absolutelyContinuous line 86
  10. lemma OAI.DirectionalTransience.Entropy.integrable_of_bounded_truncated_integrals line 111
  11. lemma OAI.DirectionalTransience.Entropy.ExpBudget.finite_kl line 140
  12. def OAI.DirectionalTransience.Entropy.logClip line 198
  13. lemma OAI.DirectionalTransience.Entropy.abs_logClip_le line 200
  14. lemma OAI.DirectionalTransience.Entropy.abs_logClip_le_abs line 204
  15. lemma OAI.DirectionalTransience.Entropy.logClip_eventually line 215
  16. lemma OAI.DirectionalTransience.Entropy.exp_logClip_log_le line 222
  17. theorem OAI.DirectionalTransience.Entropy.kl_le_of_expBudget line 237