OAI/Geometry/HyperbolicGroups/ConeData.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HyperbolicObstruction.TangentCone.catZero line 23

   Source documentation

   The constructed completed tangent cone is CAT(0).

   theorem catZero : CATZero (TangentCone h o) :=
   …

   Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.TangentCone

2. theorem OAI.HyperbolicObstruction.ConeData.segment_eq_add_scale line 36

   Source documentation

   Two-vector affine combinations in a metric cone agree with its metric segments; associativity has not been assumed.

   theorem segment_eq_add_scale (h : CATZero X) (x y : X) {t : ℝ}
       (ht : t ∈ Set.Icc (0 : ℝ) 1) :
       CATZero.segment h x y t = T.add h (T.scale (1 - t) x) (T.scale t y) := by
   …

   Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CATZero.segment

3. theorem OAI.HyperbolicObstruction.ConeData.parallel_scale line 65
4. theorem OAI.HyperbolicObstruction.ConeData.dist_opposite_translates_sq line 72

   Source documentation

   Distance between opposite translations of one point in the parallel set.

   theorem dist_opposite_translates_sq (h : CATZero X) {c d x : X}
       (hop : T.Opposite c d) (hx : T.Parallel c d x) {r s : ℝ} (hr : 0 ≤ r) (hs : 0 ≤ s) :
       dist (T.translate h c r x) (T.translate h d s x) ^ 2 =
         (r + s) ^ 2 * T.normSq c := by
   …

   Mentions: OAI.HyperbolicObstruction.CATZero

5. theorem OAI.HyperbolicObstruction.ConeData.dist_opposite_segments_sq line 84
6. theorem OAI.HyperbolicObstruction.CATZero.segment_between line 101

   Source documentation

   Restricting a chosen CAT(0) segment gives the chosen segment, including reversed subsegments.

   theorem segment_between (h : CATZero X) (x y : X) {s u t : ℝ}
       (hs : s ∈ Set.Icc (0 : ℝ) 1) (hu : u ∈ Set.Icc (0 : ℝ) 1)
       (ht : t ∈ Set.Icc (0 : ℝ) 1) :
       segment h (segment h x y s) (segment h x y u) t =
         segment h x y ((1 - t) * s + t * u) := by
   …

   Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CATZero.segment

7. theorem OAI.HyperbolicObstruction.CATZero.map_segment_of_dist line 124

   Source documentation

   A nonexpanding map that preserves one endpoint distance preserves the whole parametrized segment between those endpoints.

   theorem map_segment_of_dist {Y : Type*} [MetricSpace Y] (hX : CATZero X) (hY : CATZero Y)
       (f : X → Y) (hf : ∀ a b, dist (f a) (f b) ≤ dist a b)
       (x y : X) (hxy : dist (f x) (f y) = dist x y) {t : ℝ} (ht : t ∈ Set.Icc (0 : ℝ) 1) :
       f (segment hX x y t) = segment hY (f x) (f y) t := by
   …

   Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CATZero.segment

8. theorem OAI.HyperbolicObstruction.TangentCone.log_dist_on_segment line 146

   Source documentation

   The log based at any point of a segment is distance preserving on that segment, including pairs lying on opposite sides of the basepoint.

   theorem log_dist_on_segment (x y : X) {v s u : ℝ}
       (hv : v ∈ Set.Icc (0 : ℝ) 1) (hs : s ∈ Set.Icc (0 : ℝ) 1)
       (hu : u ∈ Set.Icc (0 : ℝ) 1) :
       dist (log h (CATZero.segment h x y v) (CATZero.segment h x y s))
         (log h (CATZero.segment h x y v) (CATZero.segment h x y u)) =
           dist (CATZero.segment h x y s) (CATZero.segment h x y u) := by
   …

   Mentions: OAI.HyperbolicObstruction.TangentCone.log, OAI.HyperbolicObstruction.CATZero.segment

9. theorem OAI.HyperbolicObstruction.TangentCone.log_dist_mid_endpoints line 175
10. theorem OAI.HyperbolicObstruction.TangentCone.opposite_mid_logs line 185
11. theorem OAI.HyperbolicObstruction.TangentCone.pairing_log_ge line 196
12. theorem OAI.HyperbolicObstruction.TangentCone.midpoint_equality_parallel line 207

    Source documentation

    Equality in the original midpoint CN comparison puts the opposite endpoint logs and the third log in their common parallel set, and the log preserves both remaining triangle sides.

    theorem midpoint_equality_parallel (o x y : X)
        (heq : dist o (CATZero.mid h x y) ^ 2 =
          (dist o x ^ 2 + dist o y ^ 2) / 2 - dist x y ^ 2 / 4) :
        (coneData h (CATZero.mid h x y)).Parallel
          (log h (CATZero.mid h x y) x) (log h (CATZero.mid h x y) y)
            (log h (CATZero.mid h x y) o) ∧
        dist (log h (CATZero.mid h x y) o) (log h (CATZero.mid h x y) x) = dist o x ∧
        dist (log h (CATZero.mid h x y) o) (log h (CATZero.mid h x y) y) = dist o y := by
    …

    Mentions: OAI.HyperbolicObstruction.CATZero.mid, OAI.HyperbolicObstruction.TangentCone.coneData, OAI.HyperbolicObstruction.TangentCone.log

13. theorem OAI.HyperbolicObstruction.TangentCone.radial_distance_of_midpoint_equality line 245

    Source documentation

    The radial distance consequence of flat-triangle rigidity, proved via the parallel set of the opposite logs at the midpoint.

    theorem radial_distance_of_midpoint_equality (o x y : X)
        (heq : dist o (CATZero.mid h x y) ^ 2 =
          (dist o x ^ 2 + dist o y ^ 2) / 2 - dist x y ^ 2 / 4)
        {t : ℝ} (ht : t ∈ Set.Icc (0 : ℝ) 1) :
        dist (CATZero.segment h o x t) (CATZero.segment h o y t) = t * dist x y := by
    …

    Mentions: OAI.HyperbolicObstruction.CATZero.mid, OAI.HyperbolicObstruction.CATZero.segment

14. theorem OAI.HyperbolicObstruction.TangentCone.log_dist_of_midpoint_equality line 267

    Source documentation

    The tangent log preserves the base side of a triangle with midpoint CN equality. This is the exact flat-triangle transfer needed by the obstruction.

    theorem log_dist_of_midpoint_equality (o x y : X)
        (heq : dist o (CATZero.mid h x y) ^ 2 =
          (dist o x ^ 2 + dist o y ^ 2) / 2 - dist x y ^ 2 / 4) :
        dist (log h o x) (log h o y) = dist x y := by
    …

    Mentions: OAI.HyperbolicObstruction.CATZero.mid, OAI.HyperbolicObstruction.TangentCone.log

15. theorem OAI.HyperbolicObstruction.TangentCone.log_mid_of_midpoint_equality line 281
16. theorem OAI.HyperbolicObstruction.CATZero.segment_reverse line 296
17. theorem OAI.HyperbolicObstruction.CATZero.mid_swap line 303
18. theorem OAI.HyperbolicObstruction.CATZero.midpoint_equality_of_interior line 310

    Source documentation

    A CN equality at any nontrivial interior point implies equality at the midpoint. The proof uses only convexity on the appropriate half-segment.

    theorem midpoint_equality_of_interior (h : CATZero X) (o x y : X) {t : ℝ}
        (ht : t ∈ Set.Ioo (0 : ℝ) 1)
        (heq : dist o (segment h x y t) ^ 2 = (1 - t) * dist o x ^ 2 + t * dist o y ^ 2 -
          t * (1 - t) * dist x y ^ 2) :
        dist o (mid h x y) ^ 2 = (dist o x ^ 2 + dist o y ^ 2) / 2 - dist x y ^ 2 / 4 := by
    …

    Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CATZero.segment, OAI.HyperbolicObstruction.CATZero.mid

19. theorem OAI.HyperbolicObstruction.TangentCone.log_dist_of_interior_equality line 345
20. theorem OAI.HyperbolicObstruction.ConeData.dist_scale line 360
21. theorem OAI.HyperbolicObstruction.ConeData.scale_segment line 366
22. theorem OAI.HyperbolicObstruction.ConeData.scale_add line 376
23. theorem OAI.HyperbolicObstruction.TangentCone.log_radial line 390
24. theorem OAI.HyperbolicObstruction.TangentCone.log_dist_of_radial_equal line 404

    Source documentation

    Equality of distances at all sufficiently small radial fractions transfers exactly to the completed tangent cone.

    theorem log_dist_of_radial_equal (o x y : X)
        (heq : ∀ t ∈ Set.Ioc (0 : ℝ) 1,
          dist (CATZero.segment h o x t) (CATZero.segment h o y t) = t * dist x y) :
        dist (log h o x) (log h o y) = dist x y := by
    …

    Mentions: OAI.HyperbolicObstruction.CATZero.segment, OAI.HyperbolicObstruction.TangentCone.log

25. theorem OAI.HyperbolicObstruction.TangentCone.log_dist_of_right_fractional line 420

    Source documentation

    The fixed-fraction angle test of the source suffices; no exchange of ultralimits and angles is used.

    theorem log_dist_of_right_fractional (o x y : X)
        (hsq : dist x y ^ 2 = dist o x ^ 2 + dist o y ^ 2)
        (hlower : ∀ t ∈ Set.Ioc (0 : ℝ) 1,
          t ^ 2 * (dist o x ^ 2 + dist o y ^ 2) ≤
            dist (CATZero.segment h o x t) (CATZero.segment h o y t) ^ 2) :
        dist (log h o x) (log h o y) = dist x y := by
    …

    Mentions: OAI.HyperbolicObstruction.CATZero.segment, OAI.HyperbolicObstruction.TangentCone.log