OAI/Probability/DirectionalWalk/DyadicBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalZeroOne.dyad line 12
2. lemma OAI.DirectionalZeroOne.dyad_pos line 14
3. lemma OAI.DirectionalZeroOne.dyad_ne_top line 15
4. lemma OAI.DirectionalZeroOne.exists_dyad_bin line 17
5. lemma OAI.DirectionalZeroOne.return_bins_cover line 44
6. lemma OAI.DirectionalZeroOne.tsum_subtype_cover line 52
7. lemma OAI.DirectionalZeroOne.half_geometric_sum_le line 66
8. lemma OAI.DirectionalZeroOne.half_geometric_tail_sum_le line 73
9. lemma OAI.DirectionalZeroOne.dyadic_weighted_mass_sum line 94
10. lemma OAI.DirectionalZeroOne.dyadic_event_weight_bound line 118