OAI/Combinatorics/ContingencyTables/Machines/InitialFactorialBits.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

One finite Boolean word for the actual initial transversal

The word is split into disjoint cell blocks; each block chooses a size and then a subset of that size. The total variation errors add before the exact paired-transversal encoding is applied.

  1. def OAI.ContingencyTables.InitialFactorialBits.bitCount line 22
  2. def OAI.ContingencyTables.InitialFactorialBits.wordEquiv line 24
  3. def OAI.ContingencyTables.InitialFactorialBits.drawChoices line 29
  4. theorem OAI.ContingencyTables.InitialFactorialBits.drawChoices_law line 33
  5. theorem OAI.ContingencyTables.InitialFactorialBits.drawChoices_error line 43
  6. theorem OAI.ContingencyTables.InitialFactorialBits.bitCount_eq line 50
  7. theorem OAI.ContingencyTables.InitialFactorialBits.bitCount_bound line 57
  8. theorem OAI.ContingencyTables.InitialFactorialBits.drawChoices_error_bound line 67
  9. def OAI.ContingencyTables.InitialFactorialBits.choiceEquiv line 83
  10. theorem OAI.ContingencyTables.InitialFactorialBits.choiceEquiv_law line 87
  11. def OAI.ContingencyTables.InitialFactorialBits.transversalDraw line 98
  12. theorem OAI.ContingencyTables.InitialFactorialBits.transversalDraw_error line 104