OAI/Probability/SKRatio/Entropy/Entropy.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatio.FiniteLaw.entropy line 14
2. def OAI.SKRatio.FiniteLaw.relativeEntropy line 17
3. lemma OAI.SKRatio.FiniteLaw.mul_log_div line 19
4. lemma OAI.SKRatio.FiniteLaw.relativeEntropy_nonneg line 25
5. lemma OAI.SKRatio.FiniteLaw.entropy_density line 38
6. lemma OAI.SKRatio.FiniteLaw.relativeEntropy_continuous line 47
7. lemma OAI.SKRatio.FiniteLaw.entropy_variational line 53
8. lemma OAI.SKRatio.FiniteLaw.event_entropy_bound line 81
9. lemma OAI.SKRatio.FiniteLaw.hellinger_pointwise line 116
10. lemma OAI.SKRatio.FiniteLaw.hellinger_le_entropy line 134
11. lemma OAI.SKRatio.FiniteLaw.totalVariation_square_le_entropy line 146
12. lemma OAI.SKRatio.Calculus.continuousKernel_balance line 177
13. def OAI.SKRatio.Calculus.transitionDensity line 186
14. lemma OAI.SKRatio.Calculus.transitionDensity_eq_semigroup line 189
15. lemma OAI.SKRatio.Calculus.transitionDensity_pos line 199
16. lemma OAI.SKRatio.Calculus.transitionDensity_mean line 202
17. lemma OAI.SKRatio.Calculus.transitionDensity_hasDerivAt line 207
18. def OAI.SKRatio.Calculus.transitionEntropy line 213
19. lemma OAI.SKRatio.Calculus.transitionEntropy_eq line 216
20. lemma OAI.SKRatio.Calculus.transitionEntropy_continuous line 225
21. lemma OAI.SKRatio.Calculus.transitionEntropy_zero line 230
22. lemma OAI.SKRatio.Calculus.transitionEntropy_hasDerivAt line 234
23. theorem OAI.SKRatio.Calculus.transitionEntropy_decay line 257
24. lemma OAI.SKRatio.Calculus.abs_hamiltonian_le_norm line 297
25. lemma OAI.SKRatio.Calculus.log_inverse_mass_le line 317
26. lemma OAI.SKRatio.Calculus.continuousDistance_square_le_entropy line 337
27. lemma OAI.SKRatio.Calculus.continuousDistance_square_decay line 347
28. theorem OAI.SKRatio.Calculus.uniform_median_upper_of_mlsi line 361