OAI/NumberTheory/TwoPoint/Walks/ForestPathCode.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TwoPointCorrelations.forest_path_support_identified line 14

   Source documentation

   The support of a path is transported exactly by a graph isomorphism.

   theorem forest_path_support_identified (e : G ≃g H) (hH : H.IsAcyclic)
       {a b : V} (p : G.Walk a b) (q : H.Walk (e a) (e b))
       (hp : p.IsPath) (hq : q.IsPath) : p.support.map e = q.support := by
   …

2. theorem OAI.TwoPointCorrelations.represented_walk_same_code line 26

   Source documentation

   Equal shape and equal endpoint indices determine the same numbered walk, independently of the numerical realization of the graph.

   theorem represented_walk_same_code [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)
       (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 _ => ()))
       (hGa : G.IsAcyclic) (hHa : H.IsAcyclic)
       {a b : V} (p : G.Walk a b)
       (q : H.Walk (forestShapeEquiv t s ht hc hs hd hshape a)
         (forestShapeEquiv t s ht hc hs hd hshape b))
       (hp : List.IsChain (· ≠ ·) p.edges) (hq : List.IsChain (· ≠ ·) q.edges) :
   …

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

3. theorem OAI.TwoPointCorrelations.represented_walk_same_endpoints line 52

   Source documentation

   Endpoint indices suffice; the graphs may have different vertex types.

   theorem represented_walk_same_endpoints [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)
       (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 _ => ()))
       (hGa : G.IsAcyclic) (hHa : H.IsAcyclic)
       {a b : V} {c d : W} (p : G.Walk a b) (q : H.Walk c d)
       (hp : List.IsChain (· ≠ ·) p.edges) (hq : List.IsChain (· ≠ ·) q.edges)
       (ha : (forestNodes t).idxOf a = (forestNodes s).idxOf c)
       (hb : (forestNodes t).idxOf b = (forestNodes s).idxOf d) :
   …

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