OAI/Probability/FKMaps/Noncrossing.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.FKCRT.MapCycles.Arches line 13

   Source documentation

   Ordered stack matching, with unpaired positions allowed. The skipped positions will be endpoints of the other colour in the map tour.

   inductive Arches : List α → List (α × α) → Prop
     | nil : Arches [] []
     | skip (a : α) {l E} : Arches l E → Arches (a :: l) E
     | pair (a b : α) {L R E F} : Arches L E → Arches R F →
         Arches (a :: (L ++ b :: R)) ((a,b) :: (E ++ F))
   
   /-- Left transpositions in traversal order. -/

2. def OAI.FKCRT.MapCycles.turns line 20

   Source documentation

   Left transpositions in traversal order.

   def turns : List (α × α) → Perm α
     | [] => 1
     | (a,b) :: E => turns E * swap a b

3. lemma OAI.FKCRT.MapCycles.turns_nil line 24
4. lemma OAI.FKCRT.MapCycles.turns_cons line 25
5. lemma OAI.FKCRT.MapCycles.turns_append line 28
6. lemma OAI.FKCRT.MapCycles.Arches.endpoints line 35
7. lemma OAI.FKCRT.MapCycles.turns_fixed line 51
8. lemma OAI.FKCRT.MapCycles.Arches.turns_fixed line 60
9. lemma OAI.FKCRT.MapCycles.formPerm_append_comm line 67
10. lemma OAI.FKCRT.MapCycles.cut_local_action line 72
11. theorem OAI.FKCRT.MapCycles.Arches.card_orbits_turns line 95

    Source documentation

    Stack/noncrossing chords attain the maximum possible cycle count. The unused initial string is arbitrary, so this also handles skipped darts and the end/start seam of a rooted tour.

    theorem Arches.card_orbits_turns [Fintype α] {l : List α} {E}
        (h : Arches l E) (Z : List α) (p : Perm α)
        (hn : (Z ++ l).Nodup)
        (hp : ∀ x ∈ Z ++ l, p x = (Z ++ l).formPerm x) :
        Nat.card (Orbits (turns E * p)) = Nat.card (Orbits p) + E.length := by
    …

    Mentions: OAI.FKCRT.MapCycles.Arches, OAI.FKCRT.MapCycles.Orbits, OAI.FKCRT.MapCycles.turns

12. lemma OAI.FKCRT.MapCycles.Arches.append line 160
13. lemma OAI.FKCRT.MapCycles.Arches.empty line 168
14. lemma OAI.FKCRT.MapCycles.cons_sublist_split line 173
15. lemma OAI.FKCRT.MapCycles.Arches.mono line 184
16. def OAI.FKCRT.MapCycles.endpoints line 199

    Source documentation

    Flatten the pair endpoints without imposing an artificial pair order.

    def endpoints (E : List (α×α)) : List α := E.flatMap (fun e => [e.1,e.2])

17. lemma OAI.FKCRT.MapCycles.endpoints_nil line 201
18. lemma OAI.FKCRT.MapCycles.endpoints_cons line 202
19. lemma OAI.FKCRT.MapCycles.endpoints_append line 204
20. theorem OAI.FKCRT.MapCycles.dyck_arches line 210

    Source documentation

    Every Dyck path, on an arbitrary ordered list of positions, has a complete noncrossing arch pairing. This is a constructive existence statement, not a planarity assumption on a map.

    theorem dyck_arches (p : DyckWord) (l : List α) (f : α→DyckStep)
        (hl : l.map f=p.toList) :
        ∃ E : List (α×α), Arches l E ∧ (endpoints E).Perm l ∧
          ∀ e∈E,f e.1=.U ∧ f e.2=.D := by
    …

    Mentions: OAI.FKCRT.MapCycles.Arches, OAI.FKCRT.MapCycles.endpoints

21. lemma OAI.FKCRT.MapCycles.mem_endpoints line 278
22. lemma OAI.FKCRT.MapCycles.turns_fixed_of_notMem line 282
23. lemma OAI.FKCRT.MapCycles.turns_pair line 289
24. lemma OAI.FKCRT.MapCycles.endpoints_pair_ne line 314
25. lemma OAI.FKCRT.MapCycles.turns_involutive line 324
26. lemma OAI.FKCRT.MapCycles.turns_self line 333
27. lemma OAI.FKCRT.MapCycles.turns_eq_self_iff line 337
28. lemma OAI.FKCRT.MapCycles.turns_mem_iff line 346
29. lemma OAI.FKCRT.MapCycles.turns_sublist_apply line 355