CanonicalForest.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Equal ordered-forest shapes identify their graphs by preorder indices.

def OAI.TwoPointCorrelations.forestIndexEquiv line 16
Source documentation
The finite index of a vertex is its first occurrence in preorder.
```
def forestIndexEquiv [DecidableEq V] (t : BinaryTree V)
    (ht : (forestNodes t).Nodup) (hc : ∀ v, v ∈ forestNodes t) :
    V ≃ Fin (forestNodes t).length :=
…
```
Mentions: OAI.TwoPointCorrelations.forestNodes
lemma OAI.TwoPointCorrelations.forestIndexEquiv_val line 21
lemma OAI.TwoPointCorrelations.forest_shape_length line 25

def OAI.TwoPointCorrelations.forestShapeEquiv line 31

Source documentation

This identification uses only the shape and the two preorder enumerations.

def forestShapeEquiv [DecidableEq V] [DecidableEq W]
    (t : BinaryTree V) (s : BinaryTree W)
    (ht : (forestNodes t).Nodup) (hc : ∀ v, v ∈ forestNodes t)
    (hs : (forestNodes s).Nodup) (hd : ∀ w, w ∈ forestNodes s)
    (hshape : t.map (fun _ => ()) = s.map (fun _ => ())) : V ≃ W :=
…

Mentions: OAI.TwoPointCorrelations.forestNodes

theorem OAI.TwoPointCorrelations.forestShapeEquiv_index line 39

theorem OAI.TwoPointCorrelations.forestShapeEquiv_adjacent line 51

Source documentation

In particular the identification preserves parent/child incidence.

theorem forestShapeEquiv_adjacent [DecidableEq V] [DecidableEq W]
    (t : BinaryTree V) (s : BinaryTree W)
    (ht : (forestNodes t).Nodup) (hc : ∀ v, v ∈ forestNodes t)
    (hs : (forestNodes s).Nodup) (hd : ∀ w, w ∈ forestNodes s)
    (hshape : t.map (fun _ => ()) = s.map (fun _ => ())) (a b : V) :
    forestAdjacent s (forestShapeEquiv t s ht hc hs hd hshape a)
      (forestShapeEquiv t s ht hc hs hd hshape b) ↔ forestAdjacent t a b := by
…

Mentions: OAI.TwoPointCorrelations.forestNodes, OAI.TwoPointCorrelations.forestAdjacent, OAI.TwoPointCorrelations.forestShapeEquiv

def OAI.TwoPointCorrelations.representedGraphIso line 62

Source documentation

A common erased shape gives an isomorphism of the represented graphs.

def representedGraphIso [DecidableEq V] [DecidableEq W]
    (G : SimpleGraph V) (H : SimpleGraph W) (t : BinaryTree V) (s : BinaryTree W)
    (ht : (forestNodes t).Nodup) (hc : ∀ v, v ∈ forestNodes t)
    (hs : (forestNodes s).Nodup) (hd : ∀ w, w ∈ forestNodes s)
    (hG : ∀ a b, forestAdjacent t a b ↔ G.Adj a b)
    (hH : ∀ a b, forestAdjacent s a b ↔ H.Adj a b)
    (hshape : t.map (fun _ => ()) = s.map (fun _ => ())) : G ≃g H where
…

Mentions: OAI.TwoPointCorrelations.forestNodes, OAI.TwoPointCorrelations.forestAdjacent