OAI/Combinatorics/ContingencyTables/Machines/PairedCatalogProgram.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Computing paired-coordinate metadata from a binary profile

Consecutive coordinates are paired by the bounded list scan (0,1),(2,3),.... This is the exact metadata of the canonical paired-label order, rather than a catalog supplied as an external oracle.

  1. def OAI.ContingencyTables.PairedCatalogProgram.indexPair line 16
  2. def OAI.ContingencyTables.PairedCatalogProgram.twiceRealizer line 18
  3. def OAI.ContingencyTables.PairedCatalogProgram.indexPairRealizer line 22
  4. lemma OAI.ContingencyTables.PairedCatalogProgram.polynomial_indexPair line 27
  5. def OAI.ContingencyTables.PairedCatalogProgram.indicesRealizer line 35
  6. lemma OAI.ContingencyTables.PairedCatalogProgram.polynomial_indices line 38
  7. def OAI.ContingencyTables.PairedCatalogProgram.catalog line 46
  8. def OAI.ContingencyTables.PairedCatalogProgram.catalogRealizer line 48
  9. theorem OAI.ContingencyTables.PairedCatalogProgram.polynomial_catalog line 50
  10. def OAI.ContingencyTables.PairedCatalogProgram.pairList line 53
  11. lemma OAI.ContingencyTables.PairedCatalogProgram.pairList_length line 57
  12. lemma OAI.ContingencyTables.PairedCatalogProgram.pairList_product line 62
  13. lemma OAI.ContingencyTables.PairedCatalogProgram.pairList_get_even line 69
  14. lemma OAI.ContingencyTables.PairedCatalogProgram.pairList_get_odd line 80
  15. def OAI.ContingencyTables.PairedCatalogProgram.labelOrder line 96
  16. lemma OAI.ContingencyTables.PairedCatalogProgram.coordinate_false line 99
  17. lemma OAI.ContingencyTables.PairedCatalogProgram.coordinate_true line 112
  18. theorem OAI.ContingencyTables.PairedCatalogProgram.catalog_encode line 127

    Source documentation

    Every state encoded in the canonical order has exactly the pair catalog computed by the polynomial consecutive-coordinate scan.

    theorem catalog_encode (S : Set (Copy b×Bool)) :
    catalog (encodeSet (CanonicalInitialEncoding.coordinateEquiv b) S)=
      List.ofFn (fun i : Fin (copyOrder b).length =>
        ((CanonicalInitialEncoding.coordinateEquiv b (labelOrder b i,false)).val,
          (CanonicalInitialEncoding.coordinateEquiv b (labelOrder b i,true)).val)) := by
…

    Mentions: OAI.ContingencyTables.PairedCatalogProgram.catalog, OAI.ContingencyTables.CanonicalInitialEncoding.coordinateEquiv, OAI.ContingencyTables.PairedCatalogProgram.labelOrder