OAI/Combinatorics/ContingencyTables/Transport/FiniteScaledDraw.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The bounded quotient draw is realized by an actual Boolean word

  1. def OAI.ContingencyTables.FairBits.scaledInteger line 16
  2. theorem OAI.ContingencyTables.FairBits.scaledIntegerLaw_eq line 21
  3. def OAI.ContingencyTables.FairBits.scaledBitInteger line 35
  4. theorem OAI.ContingencyTables.FairBits.scaledBitIntegerLaw_eq line 40

    Source documentation

    The exact law of the finite Boolean quotient operation is the law used in the dense offset error estimate and the tabulation formula.

    theorem scaledBitIntegerLaw_eq (M k : ℕ) (hM : 0 < M) :
    mapLaw (uniformLaw (α := Fin k → Bool)) (scaledBitInteger M k hM) = scaledLaw M k hM := by
…

    Mentions: OAI.ContingencyTables.FairBits.scaledBitInteger, OAI.ContingencyTables.FairBits.scaledLaw