OAI/Combinatorics/ContingencyTables/Rooted/RootedCompletion.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Forest completion with an explicit component-root selector

Only reachability and constancy on each component are needed for the integral completion. Making these data explicit permits the executed least-root selector to replace the original quotient representative, without asserting that two different selectors are equal.

  1. structure OAI.ContingencyTables.RootedCompletion.Selection line 21
  2. lemma OAI.ContingencyTables.RootedCompletion.Selection.idempotent line 26
  3. def OAI.ContingencyTables.RootedCompletion.original line 29
  4. def OAI.ContingencyTables.RootedCompletion.canonical line 34
  5. def OAI.ContingencyTables.RootedCompletion.Selection.map line 39
  6. def OAI.ContingencyTables.RootedCompletion.rowColumn line 49

    Source documentation

    The concrete row-then-column vertex order of the contingency graph.

    def rowColumn {m n : ℕ} (T : SimpleGraph (Fin m⊕Fin n)) [DecidableRel T.Adj] :
    Selection T :=
…

    Mentions: OAI.ContingencyTables.RootedCompletion.Selection

  7. lemma OAI.ContingencyTables.RootedCompletion.rowColumn_root line 53
  8. def OAI.ContingencyTables.RootedCompletion.path line 58
  9. def OAI.ContingencyTables.RootedCompletion.flow line 63
  10. lemma OAI.ContingencyTables.RootedCompletion.flow_skew line 66
  11. lemma OAI.ContingencyTables.RootedCompletion.flow_supported line 74
  12. theorem OAI.ContingencyTables.RootedCompletion.flow_divergence_all line 81
  13. theorem OAI.ContingencyTables.RootedCompletion.flow_divergence line 88
  14. def OAI.ContingencyTables.RootedCompletion.table line 101
  15. lemma OAI.ContingencyTables.RootedCompletion.table_supported line 106
  16. lemma OAI.ContingencyTables.RootedCompletion.table_row line 111
  17. lemma OAI.ContingencyTables.RootedCompletion.table_column line 125
  18. theorem OAI.ContingencyTables.RootedCompletion.zero_of_nonroot_sums line 145
  19. theorem OAI.ContingencyTables.RootedCompletion.table_unique line 201
  20. theorem OAI.ContingencyTables.RootedCompletion.table_original line 226