OAI/Combinatorics/ContingencyTables/Sampling/SmallRepairGeometryProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.ProfilePrograms.RepairGeometry line 11
2. def OAI.ContingencyTables.ProfilePrograms.sourceCell line 13
3. def OAI.ContingencyTables.ProfilePrograms.targetCell line 16
4. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_sourceCell line 19
5. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_targetCell line 23
6. def OAI.ContingencyTables.ProfilePrograms.crossingIndex line 27
7. def OAI.ContingencyTables.ProfilePrograms.crossingIndexRealizer line 30
8. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_crossingIndex line 34
9. def OAI.ContingencyTables.ProfilePrograms.capacityList line 40
10. def OAI.ContingencyTables.ProfilePrograms.capacityListRealizer line 42
11. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_capacityList line 44
12. lemma OAI.ContingencyTables.ProfilePrograms.capacityList_ofFn line 47
13. lemma OAI.ContingencyTables.SmallGraphProfiles.catalog_getD line 60
14. theorem OAI.ContingencyTables.SmallGraphProfiles.crossingIndex_eq line 67

    Source documentation

    Large crossing cells use the out-of-range index in both the forward and inverse arithmetic repairs.

    theorem crossingIndex_eq (s t : Cells small) :
        crossingIndex (cellCatalog small e,((e.symm s).val,(e.symm t).val))=
          cellIndex small e (t.val.1,s.val.2) := by
    …

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