OAI/Combinatorics/ParityLifts/BagTrees.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ParityWL.IndexedTree line 14

    Source documentation

    An ordinary finite rooted tree in topological node order.

    structure IndexedTree where
…
  2. inductive OAI.ParityWL.IndexedTree.Ancestor line 20
  3. lemma OAI.ParityWL.IndexedTree.Ancestor.le line 29
  4. lemma OAI.ParityWL.IndexedTree.Ancestor.trans line 34
  5. lemma OAI.ParityWL.IndexedTree.Ancestor.antisymm line 40
  6. lemma OAI.ParityWL.IndexedTree.Ancestor.cases' line 43
  7. lemma OAI.ParityWL.IndexedTree.Ancestor.parent line 49
  8. lemma OAI.ParityWL.IndexedTree.root_ancestor line 52
  9. lemma OAI.ParityWL.IndexedTree.ancestor_chain line 59
  10. lemma OAI.ParityWL.IndexedTree.ancestor_child line 71
  11. lemma OAI.ParityWL.IndexedTree.children_eq line 81
  12. structure OAI.ParityWL.ReducedBagTree line 104

    Source documentation

    Bags on a finite tree. Occurrences form the subtree above their unique highest occurrence top; the interval axiom is precisely subtree convexity. The intersections on nonroot edges have size strictly below the bag bound; this is the exact reduction property needed by the orientation argument.

    structure ReducedBagTree (F : SimpleGraph W) (t : ℕ) extends IndexedTree where
…

    Mentions: OAI.ParityWL.IndexedTree

  13. def OAI.ParityWL.ReducedBagTree.outer line 119
  14. def OAI.ParityWL.ReducedBagTree.cuts line 122
  15. lemma OAI.ParityWL.ReducedBagTree.mem_outer line 130
  16. lemma OAI.ParityWL.ReducedBagTree.mem_cut_separator line 134
  17. lemma OAI.ParityWL.ReducedBagTree.outer_disjoint line 138
  18. lemma OAI.ParityWL.ReducedBagTree.outside_boundary line 146
  19. lemma OAI.ParityWL.ReducedBagTree.bag_subset_cut line 166
  20. lemma OAI.ParityWL.ReducedBagTree.child_outer_disjoint_bag line 178
  21. lemma OAI.ParityWL.ReducedBagTree.child_outer_subset line 186
  22. lemma OAI.ParityWL.ReducedBagTree.branch_disjoint_bag line 195
  23. lemma OAI.ParityWL.ReducedBagTree.branch_eq line 207
  24. lemma OAI.ParityWL.ReducedBagTree.reverse_disjoint_child line 211
  25. lemma OAI.ParityWL.ReducedBagTree.branches_disjoint line 218
  26. lemma OAI.ParityWL.ReducedBagTree.branch_cover line 250
  27. def OAI.ParityWL.ReducedBagTree.toReducedCuts line 283

    Source documentation

    Extract the actual shores and local vertex partitions from the occurrence subtrees; vertices are not double-counted even if they occur in many bags.

    noncomputable def toReducedCuts : ReducedCutDecomposition F t where
…

    Mentions: OAI.ParityWL.ReducedCutDecomposition