OAI/Combinatorics/ContingencyTables/Rooted/LargeEdgeCatalogProgram.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

The executed weighted catalog of large cells

Rows and columns are indexed by their stored margin-list lengths. The catalog contains each retained large cell once, with its actual binary capacity and its row/column graph endpoints.

  1. abbrev OAI.ContingencyTables.LargeEdgeCatalogProgram.Input line 18
  2. abbrev OAI.ContingencyTables.LargeEdgeCatalogProgram.CellInput line 19
  3. def OAI.ContingencyTables.LargeEdgeCatalogProgram.vertexCount line 21
  4. def OAI.ContingencyTables.LargeEdgeCatalogProgram.vertexCountRealizer line 22
  5. lemma OAI.ContingencyTables.LargeEdgeCatalogProgram.polynomial_vertexCount line 26
  6. def OAI.ContingencyTables.LargeEdgeCatalogProgram.endpoints line 35
  7. def OAI.ContingencyTables.LargeEdgeCatalogProgram.endpointsRealizer line 36
  8. lemma OAI.ContingencyTables.LargeEdgeCatalogProgram.polynomial_endpoints line 41
  9. def OAI.ContingencyTables.LargeEdgeCatalogProgram.entry line 49
  10. def OAI.ContingencyTables.LargeEdgeCatalogProgram.entryRealizer line 50
  11. lemma OAI.ContingencyTables.LargeEdgeCatalogProgram.polynomial_entry line 51
  12. def OAI.ContingencyTables.LargeEdgeCatalogProgram.large line 54
  13. def OAI.ContingencyTables.LargeEdgeCatalogProgram.largeRealizer line 55
  14. lemma OAI.ContingencyTables.LargeEdgeCatalogProgram.polynomial_large line 57
  15. def OAI.ContingencyTables.LargeEdgeCatalogProgram.cells line 60
  16. def OAI.ContingencyTables.LargeEdgeCatalogProgram.cellsRealizer line 62
  17. lemma OAI.ContingencyTables.LargeEdgeCatalogProgram.polynomial_cells line 65
  18. def OAI.ContingencyTables.LargeEdgeCatalogProgram.catalog line 70
  19. def OAI.ContingencyTables.LargeEdgeCatalogProgram.catalogRealizer line 71
  20. lemma OAI.ContingencyTables.LargeEdgeCatalogProgram.polynomial_catalog line 73
  21. lemma OAI.ContingencyTables.LargeEdgeCatalogProgram.entry_code line 79
  22. lemma OAI.ContingencyTables.LargeEdgeCatalogProgram.mem_cells_code line 86
  23. theorem OAI.ContingencyTables.LargeEdgeCatalogProgram.mem_catalog_code line 117

    Source documentation

    Exact source cell capacities and graph endpoints, with no finite choice or supplied catalog-correctness hypothesis.

    theorem mem_catalog_code (r : Fin m→ℕ) (c : Fin n→ℕ) (b : Fin m→Fin n→ℕ)
    (W : ℕ) (e : Edge) :
    e∈catalog (NetworkVertexCode.data r c b,W) ↔
      ∃ i : Fin m,∃ j : Fin n,W≤b i j ∧ e=((i.val,m+j.val),b i j) := by
…

    Mentions: OAI.ContingencyTables.LargeEdgeCatalogProgram.catalog, OAI.ContingencyTables.NetworkVertexCode.data

  24. lemma OAI.ContingencyTables.LargeEdgeCatalogProgram.vertexCount_code line 130