OAI/Geometry/HyperbolicGroups/TangentRay.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HyperbolicObstruction.CATZero.segment_dist line 18
  2. theorem OAI.HyperbolicObstruction.CATZero.segment_mul line 23
  3. theorem OAI.HyperbolicObstruction.CATZero.radial_contraction line 37

    Source documentation

    Radial contraction, used in the construction of the tangent pseudometric.

    theorem radial_contraction (h : CATZero X) (o x y : X) {t : ℝ}
    (ht : t ∈ Set.Icc (0 : ℝ) 1) :
    dist (segment h o x t) (segment h o y t) ≤ t * dist x y := by
…

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

  4. def OAI.HyperbolicObstruction.CATZero.radialPairing line 54

    Source documentation

    A comparison scalar product at two positive positions on radial segments. Its supremum as the positions decrease is the tangent scalar product.

    def radialPairing (h : CATZero X) (o x y : X) (a b : ℝ) : ℝ :=
…

    Mentions: OAI.HyperbolicObstruction.CATZero

  5. theorem OAI.HyperbolicObstruction.CATZero.radialPairing_comm line 58
  6. theorem OAI.HyperbolicObstruction.CATZero.radialPairing_lower line 64
  7. theorem OAI.HyperbolicObstruction.CATZero.radialPairing_upper line 78
  8. theorem OAI.HyperbolicObstruction.CATZero.radialPairing_antitone_left line 99

    Source documentation

    Comparison products increase when either point moves towards the base.

    theorem radialPairing_antitone_left (h : CATZero X) (o x y : X)
    {a a' b : ℝ} (ha : 0 < a) (haa : a ≤ a') (ha' : a' ≤ 1)
    (hb : b ∈ Set.Ioc (0 : ℝ) 1) :
    radialPairing h o x y a' b ≤ radialPairing h o x y a b := by
…

    Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CATZero.radialPairing

  9. theorem OAI.HyperbolicObstruction.CATZero.radialPairing_antitone_right line 119
  10. def OAI.HyperbolicObstruction.CATZero.tangentPairing line 128

    Source documentation

    Definition by bounded supremum, so no completeness of the ambient CAT(0) space is required to form comparison products in its tangent cone.

    def tangentPairing (h : CATZero X) (o x y : X) : ℝ :=
…

    Mentions: OAI.HyperbolicObstruction.CATZero

  11. theorem OAI.HyperbolicObstruction.CATZero.tangentPairing_set_nonempty line 132
  12. theorem OAI.HyperbolicObstruction.CATZero.tangentPairing_set_bddAbove line 137
  13. theorem OAI.HyperbolicObstruction.CATZero.radialPairing_le_tangentPairing line 144
  14. theorem OAI.HyperbolicObstruction.CATZero.tangentPairing_upper line 149
  15. theorem OAI.HyperbolicObstruction.CATZero.tangentPairing_lower line 155
  16. theorem OAI.HyperbolicObstruction.CATZero.tangentPairing_comm line 160
  17. theorem OAI.HyperbolicObstruction.CATZero.tangentPairing_self line 169
  18. theorem OAI.HyperbolicObstruction.CATZero.tangentPairing_vertex line 177
  19. theorem OAI.HyperbolicObstruction.CATZero.radialPairing_tendsto line 186
  20. def OAI.HyperbolicObstruction.CATZero.tangentDist line 208

    Source documentation

    Distance between formal nonnegative multiples of two radial directions.

    def tangentDist (h : CATZero X) (o x y : X) (r s : ℝ) : ℝ :=
…

    Mentions: OAI.HyperbolicObstruction.CATZero

  21. theorem OAI.HyperbolicObstruction.CATZero.tangentDist_sq_nonneg line 212
  22. theorem OAI.HyperbolicObstruction.CATZero.tangentDist_sq line 220
  23. theorem OAI.HyperbolicObstruction.CATZero.tangentDist_comm line 226
  24. theorem OAI.HyperbolicObstruction.CATZero.tangentDist_zero_left line 233
  25. theorem OAI.HyperbolicObstruction.CATZero.tangentDist_zero_right line 240
  26. theorem OAI.HyperbolicObstruction.CATZero.tangentDist_tendsto_pos line 244
  27. theorem OAI.HyperbolicObstruction.CATZero.tangentDist_tendsto_zero_left line 273
  28. theorem OAI.HyperbolicObstruction.CATZero.tangentDist_tendsto line 289
  29. theorem OAI.HyperbolicObstruction.CATZero.tangentDist_triangle line 302
  30. theorem OAI.HyperbolicObstruction.CATZero.tangentDist_same line 313
  31. theorem OAI.HyperbolicObstruction.CATZero.tangentDist_quadrilateral line 321
  32. theorem OAI.HyperbolicObstruction.CATZero.tangentDist_radial_left line 348
  33. theorem OAI.HyperbolicObstruction.CATZero.tangentDist_radial_right line 365
  34. theorem OAI.HyperbolicObstruction.CATZero.tangentDist_le line 371

    Source documentation

    Metric form of the log comparison, for any common radial factor.

    theorem tangentDist_le (h : CATZero X) (o x y : X) {r : ℝ} (hr : 0 ≤ r) :
    tangentDist h o x y r r ≤ r * dist x y := by
…

    Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CATZero.tangentDist

  35. structure OAI.HyperbolicObstruction.TangentRay line 397

    Source documentation

    Represented directions with an arbitrary nonnegative radial length factor. Zero-distance representatives are identified by the Hausdorff completion.

    structure TangentRay (h : CATZero X) (o : X) where
…

    Mentions: OAI.HyperbolicObstruction.CATZero

  36. instance OAI.HyperbolicObstruction.TangentRay.(instance at line 404) line 404
  37. def OAI.HyperbolicObstruction.TangentRay.vertex line 411
  38. def OAI.HyperbolicObstruction.TangentRay.log line 412
  39. def OAI.HyperbolicObstruction.TangentRay.scale line 413
  40. theorem OAI.HyperbolicObstruction.TangentRay.dist_def line 415
  41. theorem OAI.HyperbolicObstruction.TangentRay.dist_sq line 418
  42. theorem OAI.HyperbolicObstruction.TangentRay.dist_vertex line 424
  43. theorem OAI.HyperbolicObstruction.TangentRay.radial_metric line 428
  44. theorem OAI.HyperbolicObstruction.TangentRay.dist_scale line 437
  45. theorem OAI.HyperbolicObstruction.TangentRay.scale_lipschitz line 444
  46. theorem OAI.HyperbolicObstruction.TangentRay.quadrilateral line 447
  47. abbrev OAI.HyperbolicObstruction.TangentCone line 457

    Source documentation

    The completed cone of represented directions, built from radial CAT(0) comparison limits rather than postulated to exist.

    abbrev TangentCone (h : CATZero X) (o : X) := Completion (TangentRay h o)
…

    Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.TangentRay