OAI/Probability/Ballisticity/Entropy/EntropyContinuousTests.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.Entropy.exp_sub_le_exp_mul line 12
2. lemma OAI.DirectionalTransience.Entropy.abs_exp_sub_le line 20
3. lemma OAI.DirectionalTransience.Entropy.abs_sub_min_le line 31
4. lemma OAI.DirectionalTransience.Entropy.continuous_exp_test_approx line 42
5. theorem OAI.DirectionalTransience.Entropy.expBudget_of_continuous line 100
6. lemma OAI.DirectionalTransience.Entropy.kl_le_of_weak_limit line 127