OAI/GroupTheory/Hyperbolic/DiscreteMetric.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Release075.Discrete.Metric line 7
  2. structure OAI.Release075.Discrete.Path line 15
  3. theorem OAI.Release075.Discrete.Path.last line 25
  4. theorem OAI.Release075.Discrete.Path.at_min line 27
  5. def OAI.Release075.Discrete.Path.Geodesic line 32
  6. def OAI.Release075.Discrete.Path.Mem line 34
  7. theorem OAI.Release075.Discrete.Path.start_mem line 36
  8. theorem OAI.Release075.Discrete.Path.end_mem line 37
  9. def OAI.Release075.Discrete.Path.nil line 39
  10. def OAI.Release075.Discrete.Path.append line 46
  11. theorem OAI.Release075.Discrete.Path.length_append line 65
  12. theorem OAI.Release075.Discrete.Path.append_at_left line 68
  13. theorem OAI.Release075.Discrete.Path.append_at_right line 76
  14. def OAI.Release075.Discrete.Path.reverse line 81
  15. def OAI.Release075.Discrete.Path.sub line 92
  16. theorem OAI.Release075.Discrete.Path.sub_at line 102
  17. theorem OAI.Release075.Discrete.Path.mem_reverse_iff line 107
  18. theorem OAI.Release075.Discrete.Path.mem_sub line 113
  19. theorem OAI.Release075.Discrete.Path.mem_append_iff line 118
  20. theorem OAI.Release075.Discrete.Path.dist_at_le line 133
  21. theorem OAI.Release075.Discrete.Path.dist_le_length line 143
  22. theorem OAI.Release075.Discrete.Path.geodesic_dist_at line 146
  23. theorem OAI.Release075.Discrete.Path.geodesic_start_dist line 159
  24. theorem OAI.Release075.Discrete.Path.geodesic_end_dist line 163
  25. theorem OAI.Release075.Discrete.Path.geodesic_reverse line 167
  26. theorem OAI.Release075.Discrete.Path.geodesic_sub line 172
  27. def OAI.Release075.Discrete.Path.integral line 176
  28. theorem OAI.Release075.Discrete.Path.integral_nil line 179
  29. theorem OAI.Release075.Discrete.Path.integral_append line 182
  30. theorem OAI.Release075.Discrete.Metric.int_dist_sub_le line 200
  31. def OAI.Release075.Discrete.Metric.tent line 207
  32. theorem OAI.Release075.Discrete.Metric.tent_nonneg line 209
  33. theorem OAI.Release075.Discrete.Metric.tent_zero line 211
  34. theorem OAI.Release075.Discrete.Metric.tent_lipschitz line 215
  35. def OAI.Release075.Discrete.Metric.form line 222
  36. theorem OAI.Release075.Discrete.Metric.form_flip line 225
  37. theorem OAI.Release075.Discrete.Metric.form_self line 229
  38. theorem OAI.Release075.Discrete.Metric.form_zero line 231
  39. theorem OAI.Release075.Discrete.Metric.form_triangle_bound line 234
  40. theorem OAI.Release075.Discrete.Path.dist_start_mem line 267
  41. theorem OAI.Release075.Discrete.Path.dist_end_mem line 273
  42. def OAI.Release075.Discrete.Path.SideNear line 276
  43. theorem OAI.Release075.Discrete.Path.SideNear.reverse line 279
  44. theorem OAI.Release075.Discrete.Path.SideNear.swap line 284
  45. theorem OAI.Release075.Discrete.Path.SideNear.reverse_left line 290
  46. theorem OAI.Release075.Discrete.Path.SideNear.reverse_right line 296
  47. def OAI.Release075.Discrete.Path.TriangleNear line 300
  48. theorem OAI.Release075.Discrete.Path.synchronous_of_near line 303
  49. theorem OAI.Release075.Discrete.Path.synchronous line 320

    Source documentation

    The elementary tripod comparison: synchronous precentral points have width O(T).

    theorem synchronous {p : Path M a b} {q : Path M b c} {s : Path M a c}
    (hp : p.Geodesic) (hq : q.Geodesic) (hs : s.Geodesic) {T i : ℕ}
    (hthin : SideNear T p q s) (hi : i ≤ (p.length+s.length-q.length)/2) :
    M.dist (p.point i) (s.point i) ≤ 4*T+2 := by
…

    Mentions: OAI.Release075.Discrete.Path, OAI.Release075.Discrete.Path.SideNear

  50. theorem OAI.Release075.Discrete.Path.integral_form_nonneg line 382
  51. theorem OAI.Release075.Discrete.Path.integral_form_quadratic line 394
  52. theorem OAI.Release075.Discrete.Path.integral_form_zero line 439
  53. def OAI.Release075.Discrete.CochainBound line 449

    Source documentation

    A linear bound on the integral, for every clipped distance cochain.

    def CochainBound (M : Metric V) (B : ℕ) : Prop :=
…

    Mentions: OAI.Release075.Discrete.Metric

  54. def OAI.Release075.Discrete.ShortBypass line 454

    Source documentation

    A geodesic arc through o, closed by a short bypass outside the open T-ball.

    def ShortBypass (M : Metric V) (T : ℕ) (o : V) (K : ℕ) : Prop :=
…

    Mentions: OAI.Release075.Discrete.Metric

  55. theorem OAI.Release075.Discrete.shortBypass_quadratic line 459