OAI/Combinatorics/ContingencyTables/Rooted/RootedCellDataProgram.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Assembling the affine input from ordinary rectangular cell arrays

The baseline and both stored views are binary natural matrices. The program reads each cell once, computes its row/column vertex indices, and constructs the offset evaluator input in row-major order.

  1. abbrev OAI.ContingencyTables.RootedCellDataProgram.Matrices line 19
  2. abbrev OAI.ContingencyTables.RootedCellDataProgram.Frame line 20
  3. abbrev OAI.ContingencyTables.RootedCellDataProgram.Input line 21
  4. abbrev OAI.ContingencyTables.RootedCellDataProgram.CellInput line 22
  5. def OAI.ContingencyTables.RootedCellDataProgram.values line 24
  6. def OAI.ContingencyTables.RootedCellDataProgram.valuesRealizer line 28
  7. lemma OAI.ContingencyTables.RootedCellDataProgram.polynomial_values line 37
  8. def OAI.ContingencyTables.RootedCellDataProgram.endpoints line 54
  9. def OAI.ContingencyTables.RootedCellDataProgram.endpointsRealizer line 56
  10. lemma OAI.ContingencyTables.RootedCellDataProgram.polynomial_endpoints line 60
  11. def OAI.ContingencyTables.RootedCellDataProgram.cellValues line 68
  12. def OAI.ContingencyTables.RootedCellDataProgram.cellValuesRealizer line 69
  13. lemma OAI.ContingencyTables.RootedCellDataProgram.polynomial_cellValues line 72
  14. def OAI.ContingencyTables.RootedCellDataProgram.coefficientInput line 76
  15. def OAI.ContingencyTables.RootedCellDataProgram.coefficientInputRealizer line 78
  16. lemma OAI.ContingencyTables.RootedCellDataProgram.polynomial_coefficientInput line 84
  17. def OAI.ContingencyTables.RootedCellDataProgram.entry line 97
  18. def OAI.ContingencyTables.RootedCellDataProgram.entryRealizer line 100
  19. lemma OAI.ContingencyTables.RootedCellDataProgram.polynomial_entry line 105
  20. def OAI.ContingencyTables.RootedCellDataProgram.baselineCell line 115
  21. def OAI.ContingencyTables.RootedCellDataProgram.baselineCellRealizer line 117
  22. lemma OAI.ContingencyTables.RootedCellDataProgram.polynomial_baselineCell line 121
  23. def OAI.ContingencyTables.RootedCellDataProgram.offsetInput line 130
  24. def OAI.ContingencyTables.RootedCellDataProgram.offsetInputRealizer line 133
  25. theorem OAI.ContingencyTables.RootedCellDataProgram.polynomial_offsetInput line 139
  26. def OAI.ContingencyTables.RootedCellDataProgram.data line 151
  27. lemma OAI.ContingencyTables.RootedCellDataProgram.values_data line 159
  28. lemma OAI.ContingencyTables.RootedCellDataProgram.coefficientInput_data line 166
  29. lemma OAI.ContingencyTables.RootedCellDataProgram.entry_data line 174
  30. theorem OAI.ContingencyTables.RootedCellDataProgram.offsetInput_data line 186