OAI/Combinatorics/ContingencyTables/Rooted/RootedBinFramesProgram.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Preparing the actual bin draws from the computed free-cell catalog

Only the capacity matrix, catalog metadata, grid coordinate list and numeric sampling parameters are supplied. The program computes each full range and bin index before invoking the proved vector draw.

  1. abbrev OAI.ContingencyTables.RootedBinFramesProgram.Input line 19

    Source documentation

    (K,(precision,dimension)) and the catalog metadata/current bin.

    abbrev Input := (ℕ×(ℕ×ℕ))×(RootedForestCatalog.Data×List ℕ)

    Mentions: OAI.ContingencyTables.RootedForestCatalog.Data

  2. def OAI.ContingencyTables.RootedBinFramesProgram.catalog line 21
  3. def OAI.ContingencyTables.RootedBinFramesProgram.catalogRealizer line 22
  4. lemma OAI.ContingencyTables.RootedBinFramesProgram.polynomial_catalog line 25
  5. def OAI.ContingencyTables.RootedBinFramesProgram.cell line 29
  6. def OAI.ContingencyTables.RootedBinFramesProgram.cellRealizer line 30
  7. lemma OAI.ContingencyTables.RootedBinFramesProgram.polynomial_cell line 32
  8. def OAI.ContingencyTables.RootedBinFramesProgram.rangeSize line 36
  9. def OAI.ContingencyTables.RootedBinFramesProgram.rangeSizeRealizer line 37
  10. lemma OAI.ContingencyTables.RootedBinFramesProgram.polynomial_rangeSize line 42
  11. def OAI.ContingencyTables.RootedBinFramesProgram.coordinate line 48
  12. def OAI.ContingencyTables.RootedBinFramesProgram.coordinateRealizer line 49
  13. lemma OAI.ContingencyTables.RootedBinFramesProgram.polynomial_coordinate line 51
  14. def OAI.ContingencyTables.RootedBinFramesProgram.item line 56
  15. def OAI.ContingencyTables.RootedBinFramesProgram.itemRealizer line 58
  16. lemma OAI.ContingencyTables.RootedBinFramesProgram.polynomial_item line 61
  17. def OAI.ContingencyTables.RootedBinFramesProgram.indices line 67
  18. def OAI.ContingencyTables.RootedBinFramesProgram.indicesRealizer line 68
  19. lemma OAI.ContingencyTables.RootedBinFramesProgram.polynomial_indices line 71
  20. def OAI.ContingencyTables.RootedBinFramesProgram.frames line 74
  21. def OAI.ContingencyTables.RootedBinFramesProgram.framesRealizer line 76
  22. theorem OAI.ContingencyTables.RootedBinFramesProgram.polynomial_frames line 78
  23. def OAI.ContingencyTables.RootedBinFramesProgram.draw line 82
  24. def OAI.ContingencyTables.RootedBinFramesProgram.drawRealizer line 83
  25. theorem OAI.ContingencyTables.RootedBinFramesProgram.polynomial_draw line 86
  26. def OAI.ContingencyTables.RootedBinFramesProgram.data line 95
  27. lemma OAI.ContingencyTables.RootedBinFramesProgram.catalog_data line 99
  28. lemma OAI.ContingencyTables.RootedBinFramesProgram.cell_data line 106
  29. lemma OAI.ContingencyTables.RootedBinFramesProgram.rangeSize_data line 116
  30. lemma OAI.ContingencyTables.RootedBinFramesProgram.item_data line 124
  31. theorem OAI.ContingencyTables.RootedBinFramesProgram.frames_data line 135