OAI/Probability/FKMaps/PlaneTrees.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.FKCRT.Inventory.CoreTree line 11

   Source documentation

   The genuine finite ordered connected-core tree. Leaves carry exactly the trivial word; every nonleaf has one child for each ordered core dart.

   inductive CoreTree where
   …

2. def OAI.FKCRT.Inventory.CoreTree.word line 17
3. lemma OAI.FKCRT.Inventory.CoreTree.word_empty line 21
4. lemma OAI.FKCRT.Inventory.CoreTree.branch_nonempty line 32
5. lemma OAI.FKCRT.Inventory.CoreTree.word_injective line 40
6. lemma OAI.FKCRT.Inventory.corner_child_short line 67
7. theorem OAI.FKCRT.Inventory.exists_core_tree line 80

   Source documentation

   The finite recursive forest construction terminates because actual corner words are strictly shorter.

   theorem exists_core_tree (w : List TypedLetter) (hw : stackTypedRun w []=some []) :
       ∃ t : CoreTree,t.word=w := by
   …

   Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Inventory.CoreTree

8. def OAI.FKCRT.Inventory.CoreTree.toWord line 105
9. lemma OAI.FKCRT.Inventory.CoreTree.toWord_bijective line 107
10. def OAI.FKCRT.Inventory.CoreTree.wordEquiv line 116

    Source documentation

    Full actual-word / normalized connected-core ordered-tree bijection.

    def wordEquiv : CoreTree ≃ EmptyTypedWord := Equiv.ofBijective toWord toWord_bijective
    …

    Mentions: OAI.FKCRT.Inventory.CoreTree, OAI.FKCRT.Inventory.EmptyTypedWord, OAI.FKCRT.Inventory.CoreTree.toWord, OAI.FKCRT.Inventory.CoreTree.toWord_bijective

11. inductive OAI.FKCRT.TreeCoding.PlaneTree line 129

    Source documentation

    Ordered rooted trees; the empty child list is an actual leaf.

    inductive PlaneTree where
    …

12. instance OAI.FKCRT.TreeCoding.(instance at line 132) line 132
13. theorem OAI.FKCRT.TreeCoding.PlaneTree.inductionMem line 135
14. def OAI.FKCRT.TreeCoding.PlaneTree.degrees line 140
15. def OAI.FKCRT.TreeCoding.PlaneTree.forestDegrees line 143
16. def OAI.FKCRT.TreeCoding.PlaneTree.build line 145
17. lemma OAI.FKCRT.TreeCoding.PlaneTree.build_append line 149
18. lemma OAI.FKCRT.TreeCoding.PlaneTree.build_degrees line 155
19. lemma OAI.FKCRT.TreeCoding.PlaneTree.build_forestDegrees line 169
20. lemma OAI.FKCRT.TreeCoding.PlaneTree.degrees_injective line 177
21. lemma OAI.FKCRT.TreeCoding.PlaneTree.forestDegrees_injective line 182
22. def OAI.FKCRT.TreeCoding.PlaneTree.incrementWord line 187
23. def OAI.FKCRT.TreeCoding.PlaneTree.SuffixNegative line 189
24. lemma OAI.FKCRT.TreeCoding.PlaneTree.suffixNegative_tail line 191
25. lemma OAI.FKCRT.TreeCoding.PlaneTree.build_correct line 195
26. lemma OAI.FKCRT.TreeCoding.PlaneTree.suffixNegative_of_excursion line 220
27. lemma OAI.FKCRT.TreeCoding.PlaneTree.exists_tree_of_excursion line 230
28. def OAI.FKCRT.TreeCoding.PlaneTree.mirror line 239

    Source documentation

    Reversal of all child orders, without imposing any symmetry on marks.

    def mirror : PlaneTree → PlaneTree
      | node ts => node (ts.reverse.map mirror)

    Mentions: OAI.FKCRT.TreeCoding.PlaneTree

29. lemma OAI.FKCRT.TreeCoding.PlaneTree.mirror_mirror line 242
30. lemma OAI.FKCRT.TreeCoding.PlaneTree.incrementWord_append line 252
31. lemma OAI.FKCRT.TreeCoding.PlaneTree.suffixNegative_append line 256
32. lemma OAI.FKCRT.TreeCoding.PlaneTree.degrees_properties line 265
33. lemma OAI.FKCRT.TreeCoding.PlaneTree.degrees_excursion line 300
34. lemma OAI.FKCRT.TreeCoding.PlaneTree.degrees_nonempty line 310
35. lemma OAI.FKCRT.TreeCoding.PlaneTree.mirror_degrees_perm line 312
36. lemma OAI.FKCRT.TreeCoding.PlaneTree.mirror_size line 320
37. lemma OAI.FKCRT.TreeCoding.PlaneTree.mirror_weight line 323
38. abbrev OAI.FKCRT.Inventory.CoreLabel line 337
39. def OAI.FKCRT.Inventory.CoreLabel.arity line 340
40. def OAI.FKCRT.Inventory.CoreTree.labels line 348
41. lemma OAI.FKCRT.Inventory.CoreTree.labels_branch line 352
42. def OAI.FKCRT.Inventory.CoreTree.degrees line 356
43. def OAI.FKCRT.Inventory.CoreTree.assemble line 358
44. def OAI.FKCRT.Inventory.CoreTree.build line 363
45. lemma OAI.FKCRT.Inventory.CoreTree.build_append line 367
46. lemma OAI.FKCRT.Inventory.CoreTree.build_labels line 373
47. lemma OAI.FKCRT.Inventory.CoreTree.labels_injective line 398
48. lemma OAI.FKCRT.Inventory.CoreTree.ofFn_getD_eq_take line 403
49. lemma OAI.FKCRT.Inventory.CoreTree.assemble_labels line 413
50. lemma OAI.FKCRT.Inventory.CoreTree.build_correct line 422
51. theorem OAI.FKCRT.Inventory.CoreTree.exists_of_excursion line 447

    Source documentation

    The actual labelled arity excursion determines exactly one connected-core ordered tree. No probabilistic independence is part of this statement.

    theorem exists_of_excursion {l : List CoreLabel}
        (h : FKCRT.TreeCoding.IsExcursionList
          (FKCRT.TreeCoding.PlaneTree.incrementWord (l.map CoreLabel.arity))) :
        ∃ T : CoreTree,T.labels=l := by
    …

    Mentions: OAI.FKCRT.Inventory.CoreLabel, OAI.FKCRT.TreeCoding.IsExcursionList, OAI.FKCRT.TreeCoding.PlaneTree.incrementWord, OAI.FKCRT.Inventory.CoreLabel.arity, OAI.FKCRT.Inventory.T, OAI.FKCRT.Inventory.CoreTree