OAI/Probability/DirectionalWalk/RenewalMass.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalZeroOne.renewalPairMass line 12
2. lemma OAI.DirectionalZeroOne.renewalPairMass_le_one line 16
3. lemma OAI.DirectionalZeroOne.window_reference_llr line 20
4. lemma OAI.DirectionalZeroOne.window_reference_entropy_bound line 74
5. lemma OAI.DirectionalZeroOne.commonDepth_integrable line 136
6. lemma OAI.DirectionalZeroOne.commonDepth_integral line 147
7. lemma OAI.DirectionalZeroOne.nthCommonList_height line 168
8. lemma OAI.DirectionalZeroOne.nthCommonList_height_ae line 175
9. lemma OAI.DirectionalZeroOne.nthCommonLaw_height_integrable line 185
10. lemma OAI.DirectionalZeroOne.nthCommonLaw_height_integral line 198
11. lemma OAI.DirectionalZeroOne.windowCommonLaw_height_integrable line 211
12. lemma OAI.DirectionalZeroOne.windowCommonLaw_height_mean line 222
13. lemma OAI.DirectionalZeroOne.window_entropy_uniform line 245
14. lemma OAI.DirectionalZeroOne.window_kl_uniform line 274
15. lemma OAI.DirectionalZeroOne.klDiv_map_equiv line 293
16. lemma OAI.DirectionalZeroOne.klDiv_product line 301
17. lemma OAI.DirectionalZeroOne.product_graph line 316