OAI/Combinatorics/ContingencyTables/Rooted/RootedCatalogGrid.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Computed catalog coordinates for the oracle grid

The executable free-cell order need not agree with Fintype.equivFin. Explicit reindexing identifies the grid exponent evaluated from the catalog-ordered list.

  1. abbrev OAI.ContingencyTables.RootedCatalogGrid.freeCount line 21
  2. def OAI.ContingencyTables.RootedCatalogGrid.coordinateEquiv line 24
  3. def OAI.ContingencyTables.RootedCatalogGrid.gridEquiv line 28
  4. lemma OAI.ContingencyTables.RootedCatalogGrid.gridEquiv_apply line 36
  5. lemma OAI.ContingencyTables.RootedCatalogGrid.gridEquiv_free line 42
  6. lemma OAI.ContingencyTables.RootedCatalogGrid.gridEdge_iff line 50
  7. theorem OAI.ContingencyTables.RootedCatalogGrid.neighbor_iff line 72
  8. def OAI.ContingencyTables.RootedCatalogGrid.naturalValues line 93
  9. theorem OAI.ContingencyTables.RootedCatalogGrid.naturalBin_grid line 97
  10. theorem OAI.ContingencyTables.RootedCatalogGrid.naturalValues_list line 104
  11. theorem OAI.ContingencyTables.RootedCatalogGrid.evaluatorInput_grid line 112
  12. theorem OAI.ContingencyTables.RootedCatalogGrid.evaluate_grid line 122

    Source documentation

    Catalog-order evaluation is exactly the grid exponent after reindexing. The runtime code never uses this equivalence.

    theorem evaluate_grid (A : Instance (Fin m) (Fin n)) (C a K : ℕ) (hC : 0 < C)
    (z : View A → ℕ) (v : Grid (I := Fin (freeCount A)) K) :
…

    Mentions: OAI.ContingencyTables.RootedCatalogGrid.freeCount