OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperComputedCatalog.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The small-cell ordering is computed from the encoded margins

  1. def OAI.ContingencyTables.SmallGraphProfiles.computedCatalog line 18
  2. lemma OAI.ContingencyTables.SmallGraphProfiles.computedCatalog_nodup line 20
  3. lemma OAI.ContingencyTables.SmallGraphProfiles.mem_computedCatalog line 23
  4. def OAI.ContingencyTables.SmallGraphProfiles.catalogCell line 42
  5. lemma OAI.ContingencyTables.SmallGraphProfiles.catalogCell_coordinates line 46
  6. lemma OAI.ContingencyTables.SmallGraphProfiles.catalogCell_bijective line 52
  7. def OAI.ContingencyTables.SmallGraphProfiles.computedCellEquiv line 67
  8. theorem OAI.ContingencyTables.SmallGraphProfiles.computedCellEquiv_catalog line 72

    Source documentation

    The proof-level cell equivalence enumerates exactly the list made by the polynomial catalog program, in the same order.

    theorem computedCellEquiv_catalog :
    cellCatalog small (computedCellEquiv r c)=computedCatalog r c := by
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.cellCatalog, OAI.ContingencyTables.SmallGraphProfiles.computedCellEquiv, OAI.ContingencyTables.SmallGraphProfiles.computedCatalog