OAI/Combinatorics/ContingencyTables/Counting/CompanionOuterWidths.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Executed phase widths and the source history word

The supplied precision markers do not contribute to the number of oracle bits. After identifying the computed scalar controls, the complete phase width is the source width plus its unused padding.

  1. lemma OAI.ContingencyTables.CompanionOuterWidths.configs_blockWidth line 19
  2. lemma OAI.ContingencyTables.CompanionOuterWidths.configs_blockWidth_reserve line 30
  3. def OAI.ContingencyTables.CompanionOuterWidths.tailWidth line 39
  4. def OAI.ContingencyTables.CompanionOuterWidths.phaseWidth line 50
  5. lemma OAI.ContingencyTables.CompanionOuterWidths.phaseWidth_reserve line 58
  6. lemma OAI.ContingencyTables.CompanionOuterWidths.initialWidth_eq line 66
  7. theorem OAI.ContingencyTables.CompanionOuterWidths.phaseWidth_source line 83