OAI/NumberTheory/TwoPoint/Bounds/LabeledForest.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Labeled ordered forests

Binary trees use the first-child / next-sibling convention. The labels are auxiliary: erasing them keeps the finite shape used by the code.

  1. def OAI.TwoPointCorrelations.forestNodes line 20
  2. def OAI.TwoPointCorrelations.forestRoots line 24
  3. def OAI.TwoPointCorrelations.forestAdjacent line 28
  4. lemma OAI.TwoPointCorrelations.forestNodes_length line 34
  5. lemma OAI.TwoPointCorrelations.forestRoots_subset line 39
  6. lemma OAI.TwoPointCorrelations.forestAdjacent_symm line 49
  7. lemma OAI.TwoPointCorrelations.forestAdjacent_mem line 55
  8. lemma OAI.TwoPointCorrelations.forestAdjacent_irrefl line 68
  9. def OAI.TwoPointCorrelations.attachForestLeaf line 83

    Source documentation

    Add a fresh leaf as the first child of its unique parent.

    def attachForestLeaf [DecidableEq V] (parent leaf : V) : BinaryTree V → BinaryTree V
  | .nil => .nil
  | .node v children siblings =>
      if v = parent then .node v (.node leaf .nil children) siblings
      else .node v (attachForestLeaf parent leaf children) (attachForestLeaf parent leaf siblings)
  10. lemma OAI.TwoPointCorrelations.attachForestLeaf_of_not_mem line 89
  11. lemma OAI.TwoPointCorrelations.attachForestLeaf_roots line 99
  12. lemma OAI.TwoPointCorrelations.attachForestLeaf_nodes_perm line 106
  13. lemma OAI.TwoPointCorrelations.move_two_disjuncts line 136
  14. lemma OAI.TwoPointCorrelations.attachForestLeaf_adjacent line 140
  15. lemma OAI.TwoPointCorrelations.attachForestLeaf_nodup line 184
  16. lemma OAI.TwoPointCorrelations.forestNodes_map line 190
  17. lemma OAI.TwoPointCorrelations.forestRoots_map line 194
  18. lemma OAI.TwoPointCorrelations.forestAdjacent_map line 198