OAI/Geometry/HyperbolicGroups/OrbitLimit.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.HyperbolicObstruction.OrbitLimit.Array line 23

   Source documentation

   Actual orbit-coordinate arrays with a uniform bound from the minimizing basepoints, before taking any product or limiting metric.

   @[ext] structure Array where
   …

2. abbrev OAI.HyperbolicObstruction.OrbitLimit.Product line 27
3. def OAI.HyperbolicObstruction.OrbitLimit.origin line 28
4. theorem OAI.HyperbolicObstruction.OrbitLimit.productCat line 31
5. def OAI.HyperbolicObstruction.OrbitLimit.boundedSection line 35
6. abbrev OAI.HyperbolicObstruction.OrbitLimit.Space line 40
7. def OAI.HyperbolicObstruction.OrbitLimit.point line 42
8. theorem OAI.HyperbolicObstruction.OrbitLimit.catZero line 43
9. lemma OAI.HyperbolicObstruction.OrbitLimit.tendsto_dist_sq line 46
10. lemma OAI.HyperbolicObstruction.OrbitLimit.dist_sq_eq line 54
11. lemma OAI.HyperbolicObstruction.OrbitLimit.dist_sq_lower line 59
12. def OAI.HyperbolicObstruction.OrbitLimit.segment line 68

    Source documentation

    Coordinate segments stay uniformly bounded.

    def segment (x y : Array (Ω := Ω) O) (t : ℝ) : Array (Ω := Ω) O :=
    …

    Mentions: OAI.HyperbolicObstruction.OrbitLimit.Array

13. lemma OAI.HyperbolicObstruction.OrbitLimit.segment_val line 89
14. lemma OAI.HyperbolicObstruction.OrbitLimit.section_segment line 94
15. lemma OAI.HyperbolicObstruction.OrbitLimit.point_segment line 108
16. lemma OAI.HyperbolicObstruction.SamplingSequence.limit_edge line 135

    Source documentation

    Every actual labelled edge has unit limiting squared length, including edges whose orientation is read backwards.

    lemma limit_edge (x y : OrbitLimit.Array (Ω := Ω) O) (e : F)
    …

    Mentions: OAI.HyperbolicObstruction.OrbitLimit.Array

17. lemma OAI.HyperbolicObstruction.SamplingSequence.limit_path line 145

    Source documentation

    The full distinct-field path estimate in the genuine mean-product ultralimit.

    lemma limit_path {G : ℕ → Type z} [∀ n, Group (G n)]
        (A : ∀ n, G n →* (X n ≃ᵢ X n)) (letter : ∀ n, L n → G n)
        (hact : ∀ n i, A n (letter n i) = (O n).isom i)
        (down : ∀ I J, I ⊆ J → Admissible J → Admissible I)
        (x y : OrbitLimit.Array (Ω := Ω) O) (σ : ∀ n, F → L n ≃ L n) (hM : 0 ≤ M)
    …

    Mentions: OAI.HyperbolicObstruction.OrbitLimit.Array

18. lemma OAI.HyperbolicObstruction.SamplingSequence.limit_fractional line 159

    Source documentation

    Fixed-fraction points pass through the product ultralimit before making any angle assertion. This is the precise exceptional ternary test.

    lemma limit_fractional {I : Finset F} {e : F} (he : e ∉ I)
        (hI : Admissible (insert e I)) (σ : ∀ n, L n ≃ L n)
        (test : ∀ n, Ω n → X n)
        (depends : ∀ n a b, (∀ i ∈ I, label n a i = label n b i) → test n a = test n b)
        {B : ℝ} (hM : 0 ≤ M) (hB : 0 ≤ B) (htest : ∀ n m, dist (O n).base (test n m) ≤ B)
        (frame : ∀ n, Ω n → X n ≃ᵢ X n)
        (o x y : OrbitLimit.Array (Ω := Ω) O)
    …

    Mentions: OAI.HyperbolicObstruction.OrbitLimit.Array