OAI/Combinatorics/ContingencyTables/Transport/RationalWalks.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.FirstSuccess.bindLaw line 15
2. def OAI.ContingencyTables.FirstSuccess.walkLaw line 25

   Source documentation

   Each transition uses a fresh independent finite experiment.

   def walkLaw (K : α → RationalLaw α) (a : α) : ℕ → RationalLaw α
     | 0 => pointLaw a
     | n + 1 => bindLaw (walkLaw K a n) K
   
   end ContingencyTables.FirstSuccess
   
   end OAI

   Mentions: OAI.ContingencyTables.FirstSuccess.pointLaw, OAI.ContingencyTables.FirstSuccess.bindLaw