OAI/Combinatorics/ContingencyTables/Transport/BooleanIntegerLaw.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Independent Boolean words combined with cached integer laws

  1. def OAI.ContingencyTables.IntegerLaw.boolean line 13
  2. lemma OAI.ContingencyTables.IntegerLaw.toRational_boolean line 17
  3. def OAI.ContingencyTables.IntegerLaw.booleanFinish line 27

    Source documentation

    A short proposal word and an independently drawn cached completion reserve their full combined word length.

    def booleanFinish {s f : ℕ} (p : IntegerLaw B (2^f))
    (finish : (Fin s → Bool) → B → C) : IntegerLaw C (2^(s+f)) :=
…

    Mentions: OAI.ContingencyTables.IntegerLaw

  4. lemma OAI.ContingencyTables.IntegerLaw.toRational_booleanFinish line 31