OAI/Probability/DirectionalWalk/ThreeLists.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DirectionalZeroOne.ThreeLists line 12
  2. def OAI.DirectionalZeroOne.splitThree line 14
  3. def OAI.DirectionalZeroOne.joinThree line 17
  4. lemma OAI.DirectionalZeroOne.split_joinThree line 22
  5. lemma OAI.DirectionalZeroOne.join_splitThree line 27
  6. def OAI.DirectionalZeroOne.splitThreeEquiv line 32
  7. def OAI.DirectionalZeroOne.oneBridgeKernel line 41
  8. def OAI.DirectionalZeroOne.signedThreeKernel line 47
  9. lemma OAI.DirectionalZeroOne.signedThreeKernel_markov line 52
  10. lemma OAI.DirectionalZeroOne.pairBridgeLaw_atom_general line 60
  11. lemma OAI.DirectionalZeroOne.threeBridgeKernel_split line 72