OAI/Probability/Ballisticity/Entropy/DominatedEntropy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.Entropy.finite_kl_of_integrable_poslog line 14
2. lemma OAI.DirectionalTransience.Entropy.finite_kl_of_domination line 46
3. lemma OAI.DirectionalTransience.StoppedWindow.sample_data_map line 99
4. def OAI.DirectionalTransience.StoppedWindow.selectedKernel line 124
5. instance OAI.DirectionalTransience.StoppedWindow.selectedKernel_markov line 127
6. lemma OAI.DirectionalTransience.StoppedWindow.selectedKernel_lintegral line 133
7. lemma OAI.DirectionalTransience.StoppedWindow.selected_reference line 149
8. lemma OAI.DirectionalTransience.StoppedWindow.selected_kl_finite line 172