OAI/Combinatorics/ContingencyTables/Counting/EstimatorWordBanks.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The exact disjoint word layout of one weight estimator

There is one bank of ratio samples for every phase, followed by one bank of correction samples. Each correction sample has its own walk and bin words. This is the literal layout used by the executable allocator.

  1. abbrev OAI.ContingencyTables.EstimatorWordBanks.Banks line 18
  2. def OAI.ContingencyTables.EstimatorWordBanks.wordEquiv line 22
  3. lemma OAI.ContingencyTables.EstimatorWordBanks.ratio_chunks line 30
  4. lemma OAI.ContingencyTables.EstimatorWordBanks.ratio_rows line 38
  5. lemma OAI.ContingencyTables.EstimatorWordBanks.correction_chunks line 44
  6. lemma OAI.ContingencyTables.EstimatorWordBanks.correction_take line 52
  7. lemma OAI.ContingencyTables.EstimatorWordBanks.correction_drop line 60