OAI/Combinatorics/ContingencyTables/Machines/FixedCardinalityBits.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Bounded Boolean implementation of fixed-cardinality subset draws

  1. def OAI.ContingencyTables.FixedCardinalityBits.headDraw line 17
  2. def OAI.ContingencyTables.FixedCardinalityBits.roundedHeadLaw line 20
  3. lemma OAI.ContingencyTables.FixedCardinalityBits.roundedHead_true line 23
  4. lemma OAI.ContingencyTables.FixedCardinalityBits.bool_variation line 40
  5. theorem OAI.ContingencyTables.FixedCardinalityBits.roundedHead_error line 50
  6. def OAI.ContingencyTables.FixedCardinalityBits.roundedFixedLaw line 58
  7. theorem OAI.ContingencyTables.FixedCardinalityBits.roundedFixed_error line 63
  8. def OAI.ContingencyTables.FixedCardinalityBits.draw line 80
  9. theorem OAI.ContingencyTables.FixedCardinalityBits.consWordLaw line 86
  10. theorem OAI.ContingencyTables.FixedCardinalityBits.draw_law line 98
  11. def OAI.ContingencyTables.FixedCardinalityBits.blockWords line 128
  12. def OAI.ContingencyTables.FixedCardinalityBits.bitDraw line 131
  13. theorem OAI.ContingencyTables.FixedCardinalityBits.bitDraw_law line 134
  14. theorem OAI.ContingencyTables.FixedCardinalityBits.bitDraw_error line 144

    Source documentation

    Exactly nB fair bits implement the sequential subset draw with total variation error at most n/2^B, uniformly in the requested size.

    theorem bitDraw_error (B n k : ℕ) :
    variation (mapLaw (uniformLaw (α := Fin (n*B) → Bool)) (bitDraw B n k))
…

    Mentions: OAI.ContingencyTables.FixedCardinalityBits.bitDraw