OAI/Probability/DirectionalWalk/ThreeChunks.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalZeroOne.interlace line 12
2. lemma OAI.DirectionalZeroOne.compProd_product line 18
3. lemma OAI.DirectionalZeroOne.graph_product_kl line 38
4. abbrev OAI.DirectionalZeroOne.ThreeChunk line 59
5. def OAI.DirectionalZeroOne.threeChunkLaw line 61
6. instance OAI.DirectionalZeroOne.threeChunkLaw_probability line 66
7. def OAI.DirectionalZeroOne.threeHeight line 72
8. def OAI.DirectionalZeroOne.threeBridgeKernel line 75
9. lemma OAI.DirectionalZeroOne.threeBridgeKernel_markov line 80
10. lemma OAI.DirectionalZeroOne.threeChunk_kl_uniform line 89