OAI/Probability/FKMaps/RootedLaw.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FKCRT.spanningGraphRelabel line 11
2. lemma OAI.FKCRT.mapConditions_relabel line 40
3. def OAI.FKCRT.relabelMap line 51
4. lemma OAI.FKCRT.relabelMap_iso line 54
5. def OAI.FKCRT.canonicalizeTree line 60

   Source documentation

   Actual tree tours put every map/tree pair into the rooted normal form.

   def canonicalizeTree (M : LabelledMap n) (T : Finset (Orbit M.val.1))
       (hT : T∈treeExtensions M.val.1 M.val.2 ∅ Finset.univ) : CanonicalTreeMap n := by
   …

   Mentions: OAI.FKCRT.LabelledMap, OAI.FKCRT.Orbit, OAI.FKCRT.treeExtensions, OAI.FKCRT.CanonicalTreeMap

6. lemma OAI.FKCRT.sameCycle_intertwine line 80
7. def OAI.FKCRT.isoOrbit line 99
8. lemma OAI.FKCRT.isoOrbit_apply line 102
9. lemma OAI.FKCRT.partialReversal_intertwine line 105
10. lemma OAI.FKCRT.treeExtension_of_tour line 115
11. def OAI.FKCRT.CanonicalTreeMap.toMap line 122
12. lemma OAI.FKCRT.CanonicalTreeMap.tour_connected line 125
13. lemma OAI.FKCRT.CanonicalTreeMap.tree line 132
14. lemma OAI.FKCRT.canonicalizeTree_of_iso line 137

    Source documentation

    Normalization respects a literal rooted map/tree isomorphism. The root condition removes the cyclic seam ambiguity, rather than dividing by it.

    lemma canonicalizeTree_of_iso (M : LabelledMap n) (T : Finset (Orbit M.val.1))
        (hT : T∈treeExtensions M.val.1 M.val.2 ∅ Finset.univ)
        (X : CanonicalTreeMap n) (r : Perm (Dart n)) (hr : r 0=0)
        (ha : ∀ d,M.val.1 (r d)=r (X.a d)) (hs : ∀ d,M.val.2 (r d)=r (X.s d))
        (hA : ∀ d,orbit X.a d∈X.A ↔ orbit M.val.1 (r d)∈T) :
        canonicalizeTree M T hT=X := by
    …

    Mentions: OAI.FKCRT.LabelledMap, OAI.FKCRT.Orbit, OAI.FKCRT.treeExtensions, OAI.FKCRT.CanonicalTreeMap, OAI.FKCRT.Dart, OAI.FKCRT.orbit, OAI.FKCRT.canonicalizeTree

15. lemma OAI.FKCRT.canonical_root_fiber_surjective line 181

    Source documentation

    Each rooted isomorphism class has its actual spanning trees as the fibre of the canonical tree representation (existence half).

    lemma canonical_root_fiber_surjective (M : LabelledMap n) (X : CanonicalTreeMap n)
        (h : MapIso X.toMap M) :
        ∃ (T : Finset (Orbit M.val.1)) (hT : T∈treeExtensions M.val.1 M.val.2 ∅ Finset.univ),
          canonicalizeTree M T hT=X := by
    …

    Mentions: OAI.FKCRT.LabelledMap, OAI.FKCRT.CanonicalTreeMap, OAI.FKCRT.MapIso, OAI.FKCRT.Orbit, OAI.FKCRT.treeExtensions, OAI.FKCRT.canonicalizeTree

16. lemma OAI.FKCRT.canonicalizeTree_iso line 212
17. lemma OAI.FKCRT.canonicalizeTree_class line 217
18. lemma OAI.FKCRT.canonicalizeTree_mem line 224
19. lemma OAI.FKCRT.canonicalizeTree_injective line 231
20. abbrev OAI.FKCRT.RootedSpanningTree line 272
21. def OAI.FKCRT.rootedTreeNormal line 275
22. lemma OAI.FKCRT.rootedTreeNormal_bijective line 278
23. def OAI.FKCRT.rootedCanonicalEquiv line 304

    Source documentation

    Actual root-isomorphism classes with actual spanning trees, not labelled objects divided by an unproved automorphism factor.

    def rootedCanonicalEquiv (n : ℕ) : RootedSpanningTree n ≃ CanonicalTreeMap n :=
    …

    Mentions: OAI.FKCRT.RootedSpanningTree, OAI.FKCRT.CanonicalTreeMap

24. def OAI.FKCRT.rootedWordEquiv line 308

    Source documentation

    Exact finite rooted-map/spanning-tree to identified-word correspondence.

    def rootedWordEquiv (n : ℕ) : RootedSpanningTree n ≃ SuccessfulWord n :=
    …

    Mentions: OAI.FKCRT.RootedSpanningTree, OAI.FKCRT.SuccessfulWord

25. lemma OAI.FKCRT.edge_reachable_rep line 321
26. lemma OAI.FKCRT.relabelEdges_erase line 330
27. lemma OAI.FKCRT.fundamentalCross_relabel line 337
28. lemma OAI.FKCRT.edgeFirst_rep line 364
29. lemma OAI.FKCRT.canonicalizeTree_rank line 374
30. theorem OAI.FKCRT.canonicalizeTree_activity line 401

    Source documentation

    Forced FK exponents are unchanged by the true rooted normal form.

    theorem canonicalizeTree_activity (M : LabelledMap n) (T : Finset (Orbit M.val.1))
        (hT : T∈treeExtensions M.val.1 M.val.2 ∅ Finset.univ) :
        explorationActivity (canonicalizeTree M T hT).a (canonicalizeTree M T hT).s
          (tourSelector (canonicalizeTree M T hT).a (canonicalizeTree M T hT).s (canonicalizeTree M T hT).valid.1) ∅ Finset.univ
          (canonicalizeTree M T hT).A (Fintype.card (Orbit (canonicalizeTree M T hT).a)) =
        explorationActivity M.val.1 M.val.2 (tourSelector M.val.1 M.val.2 M.property.1) ∅ Finset.univ
          T (Fintype.card (Orbit M.val.1)) := by
    …

    Mentions: OAI.FKCRT.LabelledMap, OAI.FKCRT.Orbit, OAI.FKCRT.treeExtensions, OAI.FKCRT.explorationActivity, OAI.FKCRT.canonicalizeTree, OAI.FKCRT.tourSelector