OAI/Combinatorics/ContingencyTables/Machines/BinVectorProgram.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

The executed independent bin-coordinate draws

Each coordinate reserves a width determined by its full range, and uses only the prefix needed by the selected interval. The implementation splits one Boolean list and performs binary arithmetic per coordinate.

  1. abbrev OAI.ContingencyTables.BinVectorProgram.Frame line 19

    Source documentation

    The interval input together with accuracy and dimension allowances.

    abbrev Frame := BinIntervalProgram.Input×(ℕ×ℕ)

    Mentions: OAI.ContingencyTables.BinIntervalProgram.Input

  2. def OAI.ContingencyTables.BinVectorProgram.reservedWidth line 21
  3. def OAI.ContingencyTables.BinVectorProgram.reservedWidthRealizer line 22
  4. lemma OAI.ContingencyTables.BinVectorProgram.polynomial_reservedWidth line 32
  5. def OAI.ContingencyTables.BinVectorProgram.activeWidth line 41
  6. def OAI.ContingencyTables.BinVectorProgram.activeWidthRealizer line 43
  7. lemma OAI.ContingencyTables.BinVectorProgram.polynomial_activeWidth line 55
  8. def OAI.ContingencyTables.BinVectorProgram.coordinate line 64
  9. def OAI.ContingencyTables.BinVectorProgram.coordinateRealizer line 66
  10. lemma OAI.ContingencyTables.BinVectorProgram.polynomial_coordinate line 72
  11. lemma OAI.ContingencyTables.BinVectorProgram.intervalSize_le line 78
  12. lemma OAI.ContingencyTables.BinVectorProgram.active_le_reserved line 85
  13. lemma OAI.ContingencyTables.BinVectorProgram.take_ofFn_prefix line 92
  14. theorem OAI.ContingencyTables.BinVectorProgram.coordinate_ofFn line 99
  15. abbrev OAI.ContingencyTables.BinVectorProgram.Input line 111
  16. def OAI.ContingencyTables.BinVectorProgram.widths line 113
  17. def OAI.ContingencyTables.BinVectorProgram.widthsRealizer line 114
  18. lemma OAI.ContingencyTables.BinVectorProgram.polynomial_widths line 115
  19. def OAI.ContingencyTables.BinVectorProgram.item line 118
  20. def OAI.ContingencyTables.BinVectorProgram.itemRealizer line 120
  21. lemma OAI.ContingencyTables.BinVectorProgram.polynomial_item line 128
  22. def OAI.ContingencyTables.BinVectorProgram.indices line 137
  23. def OAI.ContingencyTables.BinVectorProgram.indicesRealizer line 138
  24. lemma OAI.ContingencyTables.BinVectorProgram.polynomial_indices line 139
  25. def OAI.ContingencyTables.BinVectorProgram.output line 146
  26. def OAI.ContingencyTables.BinVectorProgram.outputRealizer line 147
  27. theorem OAI.ContingencyTables.BinVectorProgram.polynomial_output line 149
  28. theorem OAI.ContingencyTables.BinVectorProgram.output_ofFn line 153