OAI/Probability/Ballisticity/Entropy/OccupationEntropy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.Entropy.restricted_exp_test line 13
2. def OAI.DirectionalTransience.Entropy.activeSum line 41
3. instance OAI.DirectionalTransience.Entropy.activeSum_finite line 44
4. lemma OAI.DirectionalTransience.Entropy.activeSum_integral line 49
5. lemma OAI.DirectionalTransience.Entropy.activeSum_mass line 56
6. theorem OAI.DirectionalTransience.Entropy.activeSum_exp_test line 62
7. theorem OAI.DirectionalTransience.Entropy.normalized_activeSum_kl_le line 79