OAI/Combinatorics/ContingencyTables/Sampling/SmallCellIndexProgram.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Executable indices for small cells and their crossing cells

  1. def OAI.ContingencyTables.ProfilePrograms.cellLookupRealizer line 11
  2. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_cellLookup line 14
  3. def OAI.ContingencyTables.SmallGraphProfiles.cellCatalog line 26
  4. lemma OAI.ContingencyTables.SmallGraphProfiles.cellCatalog_nodup line 29
  5. lemma OAI.ContingencyTables.SmallGraphProfiles.mem_cellCatalog line 36
  6. theorem OAI.ContingencyTables.SmallGraphProfiles.cellCatalog_index line 50

    Source documentation

    Ordinary list search gives precisely the semantic small-cell index; large crossing cells get the out-of-range index without extra cases.

    theorem cellCatalog_index (t : Fin m×Fin n) :
    (cellCatalog small e).idxOf (t.1.val,t.2.val)=cellIndex small e t := by
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.cellCatalog, OAI.ContingencyTables.SmallGraphProfiles.cellIndex