OAI/Analysis/ForestSpace/Trees.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ForestSpace.Word line 16

   Source documentation

   Finite words, ordered by extension, including the empty root.

   Also declared: ComparatorChallenges/ForestSpace.lean:347 (same declaration text).

   structure Word where
   …

2. theorem OAI.ForestSpace.Word.ext line 21
3. instance OAI.ForestSpace.Word.(instance at line 23) line 23
4. instance OAI.ForestSpace.Word.(instance at line 24) line 24
5. instance OAI.ForestSpace.Word.(instance at line 27) line 27
6. theorem OAI.ForestSpace.Word.le_def line 35
7. theorem OAI.ForestSpace.Word.forestOrder line 36
8. theorem OAI.ForestSpace.Word.finiteAncestors line 42
9. def OAI.ForestSpace.Word.root line 47
10. def OAI.ForestSpace.Word.child line 48
11. theorem OAI.ForestSpace.Word.le_child line 50
12. theorem OAI.ForestSpace.Word.child_not_le line 51
13. theorem OAI.ForestSpace.Word.child_injective line 57
14. theorem OAI.ForestSpace.Word.le_child_iff line 62
15. theorem OAI.ForestSpace.Word.ancestor_finset_child line 78
16. theorem OAI.ForestSpace.Word.path_child line 84
17. theorem OAI.ForestSpace.Word.weakNull_path_children line 91
18. theorem OAI.ForestSpace.word_auc_modulus_zero line 100

    Source documentation

    The James-tree coordinate completion has zero AUC modulus at exactly the comparison scale for every equivalent norm; reflexivity is not assumed.

     theorem word_auc_modulus_zero {α β : ℝ} (R : EquivalentNorm (X Word) α β) :
        aucModulus (X Word) R.N (α/(2*β)) = 0 := by
    …

    Mentions: OAI.ForestSpace.EquivalentNorm, OAI.ForestSpace.X, OAI.ForestSpace.Word, OAI.ForestSpace.aucModulus

19. structure OAI.ForestSpace.Vertex line 118

    Source documentation

    A disjoint forest: one copy of Nat^{≤h} for every h≥1.

    Also declared: ComparatorChallenges/ForestSpace.lean:364 (same declaration text).

    structure Vertex where
    …

20. theorem OAI.ForestSpace.Vertex.ext line 126
21. instance OAI.ForestSpace.Vertex.(instance at line 128) line 128
22. instance OAI.ForestSpace.Vertex.(instance at line 132) line 132
23. theorem OAI.ForestSpace.Vertex.le_def line 140
24. theorem OAI.ForestSpace.Vertex.forestOrder line 141
25. theorem OAI.ForestSpace.Vertex.finiteAncestors line 147
26. def OAI.ForestSpace.Vertex.node line 155
27. def OAI.ForestSpace.Vertex.child line 158
28. theorem OAI.ForestSpace.Vertex.child_injective line 163
29. instance OAI.ForestSpace.Vertex.(instance at line 168) line 168
30. theorem OAI.ForestSpace.Vertex.child_not_le line 172
31. theorem OAI.ForestSpace.Vertex.le_child_iff line 175
32. theorem OAI.ForestSpace.Vertex.ancestor_finset_child line 186
33. theorem OAI.ForestSpace.Vertex.path_child line 192
34. def OAI.ForestSpace.Vertex.treePath line 200

    Source documentation

    A total extension of the path vector; the off-tree values are never used.

    noncomputable def treePath (h : ℕ) (s : List ℕ) : X Vertex :=
    …

    Mentions: OAI.ForestSpace.X, OAI.ForestSpace.Vertex

35. theorem OAI.ForestSpace.Vertex.norm_treePath line 204
36. theorem OAI.ForestSpace.Vertex.treePath_child line 209
37. theorem OAI.ForestSpace.finite_forest_auc_modulus_zero line 218