OAI/Analysis/DiamondDistortion/ForestModels.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DiamondDistortion.ForestNode line 13

   Also declared: ComparatorChallenges/DiamondDistortion.lean:236 (same declaration text).

2. def OAI.DiamondDistortion.ForestAncestor line 15

   Also declared: ComparatorChallenges/DiamondDistortion.lean:238 (same declaration text).

3. def OAI.DiamondDistortion.forestAncestry line 18

   Also declared: ComparatorChallenges/DiamondDistortion.lean:241 (same declaration text).

4. def OAI.DiamondDistortion.forestSegments line 31

   Also declared: ComparatorChallenges/DiamondDistortion.lean:254 (same declaration text).

5. def OAI.DiamondDistortion.infiniteAncestry line 35

   Source documentation

   Prefix order on all finite words, explicitly distinct from their lexicographic order.

   Also declared: ComparatorChallenges/DiamondDistortion.lean:258 (same declaration text).

   @[instance_reducible] def infiniteAncestry : Ancestry (List ℕ) where
   …

   Mentions: OAI.DiamondDistortion.Ancestry

6. def OAI.DiamondDistortion.infiniteSegments line 44

   Source documentation

   The infinite-height tree of all finite words; this includes the empty root.

   Also declared: ComparatorChallenges/DiamondDistortion.lean:267 (same declaration text).

   def infiniteSegments : SegmentSystem (List ℕ) :=
   …

   Mentions: OAI.DiamondDistortion.SegmentSystem

7. lemma OAI.DiamondDistortion.infinite_finite_heads line 47
8. lemma OAI.DiamondDistortion.forest_finite_heads line 55
9. def OAI.DiamondDistortion.Forest.component line 68
10. lemma OAI.DiamondDistortion.Forest.same_component line 70
11. lemma OAI.DiamondDistortion.Forest.segment_card_le line 76
12. lemma OAI.DiamondDistortion.Forest.primal_sq_bounded_components line 97
13. def OAI.DiamondDistortion.Forest.coefficients line 113
14. lemma OAI.DiamondDistortion.Forest.coefficients_bounded line 116
15. lemma OAI.DiamondDistortion.Forest.finite_component_tail line 152
16. lemma OAI.DiamondDistortion.Forest.component_set_ancestral line 183
17. lemma OAI.DiamondDistortion.Forest.full_dual_approximation line 195

    Source documentation

    The full finite-height forest dual really has finite ancestral head approximation. Both the component tail and coordinate tail arguments are proved from its disjoint-segment norm, rather than imposed as hypotheses.

    lemma full_dual_approximation (x : forestSegments.Dual) {ε : ℝ} (hε : 0 < ε) :
        ∃ H : Finset ForestNode, Ancestry.Ancestral (A := forestAncestry) (H : Set ForestNode) ∧
    …

    Mentions: OAI.DiamondDistortion.ForestNode, OAI.DiamondDistortion.Ancestry.Ancestral, OAI.DiamondDistortion.forestAncestry

18. abbrev OAI.DiamondDistortion.ForestDual line 271

    Also declared: ComparatorChallenges/DiamondDistortion.lean:270 (same declaration text).

19. abbrev OAI.DiamondDistortion.InfinitePredual line 272

    Also declared: ComparatorChallenges/DiamondDistortion.lean:271 (same declaration text).