OAI/Combinatorics/ContingencyTables/Transport/ListBitProposal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.FairBits.listBitDraw line 15

   Source documentation

   Read a binary index; every index beyond the list gives a hold.

   def listBitDraw (xs : List X) (k : ℕ) (bits : Fin k → Bool) : Option X :=
   …

2. lemma OAI.ContingencyTables.FairBits.listIndex_eq_iff line 19
3. lemma OAI.ContingencyTables.FairBits.listIndex_mass line 31
4. theorem OAI.ContingencyTables.FairBits.listBitDraw_mass line 50

   Source documentation

   This implementation has exactly the same masses as a uniform injection into the dyadic code space, with no search for that injection.

   theorem listBitDraw_mass (xs : List X) (hn : xs.Nodup) (k : ℕ)
       (hlen : xs.length ≤ 2^k) (x : X) :
       (mapLaw (uniformLaw (α := Fin k → Bool)) (listBitDraw xs k)).mass (some x)=
   …

   Mentions: OAI.ContingencyTables.FairBits.listBitDraw

5. theorem OAI.ContingencyTables.FairBits.listBitDraw_mass_decidableEq line 62