OAI/Combinatorics/ContingencyTables/Rooted/RootedCutReindex.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact canonical cut flags in the row-then-column vertex encoding

  1. lemma OAI.ContingencyTables.RootedCutReindex.delete_comap line 15
  2. lemma OAI.ContingencyTables.RootedCutReindex.reachable_comap line 21
  3. lemma OAI.ContingencyTables.RootedCutReindex.away_comap line 31
  4. lemma OAI.ContingencyTables.RootedCutReindex.cut_comap line 37
  5. lemma OAI.ContingencyTables.RootedCutReindex.canonicalCut_treeCut line 45

    Source documentation

    The Boolean program computes exactly the selected-root tree cut used in the affine coefficient, with the concrete row/column order.

    lemma canonicalCut_treeCut {m n : ℕ} (T : SimpleGraph (Fin m⊕Fin n))
    [DecidableRel T.Adj] (t : GraphCompletionCounts.TreeCell T) (a : Fin m⊕Fin n) :
    FiniteGraphCutProgram.canonicalCutCode
      ((FiniteGraphRootProgram.graphCode (T.comap finSumFinEquiv.symm),
        ((finSumFinEquiv (m := m) (n := n) (.inl t.val.1)).val,(finSumFinEquiv (m := m) (n := n) (.inr t.val.2)).val)),
…

    Mentions: OAI.ContingencyTables.GraphCompletionCounts.TreeCell, OAI.ContingencyTables.FiniteGraphCutProgram.canonicalCutCode, OAI.ContingencyTables.FiniteGraphRootProgram.graphCode