OAI/Combinatorics/ContingencyTables/Transport/CanonicalIntegerLaw.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The exact finite integer law of the normalized Boolean sampler

  1. def OAI.ContingencyTables.DensePrograms.canonicalCounts line 17
  2. theorem OAI.ContingencyTables.DensePrograms.canonicalCounts_law line 25
  3. theorem OAI.ContingencyTables.DensePrograms.canonicalCounts_computed line 57
  4. def OAI.ContingencyTables.DensePrograms.paddedCanonicalCounts line 64

    Source documentation

    A reserved word contributes a power of two for its unused suffix.

    def paddedCanonicalCounts (N : ℕ) (hN : normalizedDrawBits R P d h≤N) :
    IntegerLaw (Table R P) (2^N) :=
…

    Mentions: OAI.ContingencyTables.DensePrograms.normalizedDrawBits, OAI.ContingencyTables.IntegerLaw, OAI.ContingencyTables.Table

  5. theorem OAI.ContingencyTables.DensePrograms.paddedCanonicalCounts_law line 69