OAI/Probability/DirectionalWalk/DyadicCover.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalZeroOne.dyadic_band_cover line 12
2. lemma OAI.DirectionalZeroOne.coveredDepthBand_le_index_sum line 26
3. lemma OAI.DirectionalZeroOne.sum_shift_four_sub line 52
4. lemma OAI.DirectionalZeroOne.sum_shift_four_le line 65
5. lemma OAI.DirectionalZeroOne.log_nat_pow_two_add_one line 73
6. lemma OAI.DirectionalZeroOne.entropy_dyadic_telescope line 84
7. lemma OAI.DirectionalZeroOne.kl_event_scale_bound line 116
8. lemma OAI.DirectionalZeroOne.placed_cut_positive line 145
9. lemma OAI.DirectionalZeroOne.experiment_probability line 155
10. lemma OAI.DirectionalZeroOne.reference_probability line 162
11. lemma OAI.DirectionalZeroOne.placed_reference_summable line 174
12. lemma OAI.DirectionalZeroOne.placed_kl_bounds line 224
13. lemma OAI.DirectionalZeroOne.commonBand_entropy_upper line 290
14. lemma OAI.DirectionalZeroOne.commonBand_lower_real line 339