OAI/Probability/DirectionalWalk/RelativeContinuation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalZeroOne.relativeContinuationLaw line 12
2. lemma OAI.DirectionalZeroOne.relativeContinuationLaw_probability line 15
3. lemma OAI.DirectionalZeroOne.relativeContinuation_fresh_stopped line 20
4. lemma OAI.DirectionalZeroOne.posterior_old_prefix_contact_bound line 50
5. lemma OAI.DirectionalZeroOne.binary_cross_entropy_bound line 68
6. lemma OAI.DirectionalZeroOne.kl_event_bound line 94
7. lemma OAI.DirectionalZeroOne.posterior_cylinder_mass line 125
8. lemma OAI.DirectionalZeroOne.relativeContinuation_fresh_cylinder line 136
9. lemma OAI.DirectionalZeroOne.prefix_relative_completion_mass line 159
10. lemma OAI.DirectionalZeroOne.posterior_old_prefix_weighted_bound line 169