OAI/Geometry/HyperbolicGroups/TangentCone.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.TangentCone.vertex line 22
2. def OAI.HyperbolicObstruction.TangentCone.log line 23
3. def OAI.HyperbolicObstruction.TangentCone.scaleN line 24
4. theorem OAI.HyperbolicObstruction.TangentCone.scaleN_coe line 27
5. theorem OAI.HyperbolicObstruction.TangentCone.continuous_scaleN line 31
6. theorem OAI.HyperbolicObstruction.TangentCone.scaleN_zero line 33
7. theorem OAI.HyperbolicObstruction.TangentCone.scaleN_one line 42
8. theorem OAI.HyperbolicObstruction.TangentCone.radial_metric line 51
9. def OAI.HyperbolicObstruction.TangentCone.coneData line 65

   Source documentation

   The required radial metric law, with no asserted CAT(0) axiom. The CAT(0) property is a separate construction below.

   def coneData : ConeData (TangentCone h o) where
   …

   Mentions: OAI.HyperbolicObstruction.ConeData, OAI.HyperbolicObstruction.TangentCone

10. theorem OAI.HyperbolicObstruction.TangentCone.dist_log_le line 74
11. theorem OAI.HyperbolicObstruction.TangentCone.log_lipschitz line 79
12. theorem OAI.HyperbolicObstruction.TangentCone.dist_vertex_log line 84
13. theorem OAI.HyperbolicObstruction.TangentCone.normSq_log line 88
14. theorem OAI.HyperbolicObstruction.TangentCone.pairing_log line 92
15. theorem OAI.HyperbolicObstruction.midpoint_limit line 109

    Source documentation

    Quadrilateral comparison and approximate midpoints give a convergent midpoint sequence in a complete metric space.

    theorem midpoint_limit {Y : Type*} [MetricSpace Y] [CompleteSpace Y]
        (quad : ∀ a b c d : Y, dist a c ^ 2 + dist b d ^ 2 ≤
          dist a b ^ 2 + dist b c ^ 2 + dist c d ^ 2 + dist d a ^ 2)
        (x y : Y) (u : ℕ → Y) (b : ℕ → ℝ)
        (hb : Tendsto b atTop (𝓝 (dist x y)))
        (hu : ∀ᶠ n in atTop, dist x (u n) ≤ b n / 2 ∧ dist y (u n) ≤ b n / 2) :
        ∃ m, Tendsto u atTop (𝓝 m) ∧ dist x m = dist x y / 2 ∧
          dist y m = dist x y / 2 := by
    …

16. def OAI.HyperbolicObstruction.TangentCone.atScale line 152
17. def OAI.HyperbolicObstruction.TangentCone.rescale line 155
18. theorem OAI.HyperbolicObstruction.TangentCone.rescale_atScale line 158
19. theorem OAI.HyperbolicObstruction.TangentCone.dist_rescale_le line 170
20. def OAI.HyperbolicObstruction.TangentCone.shrink line 178
21. theorem OAI.HyperbolicObstruction.TangentCone.shrink_pos line 180
22. theorem OAI.HyperbolicObstruction.TangentCone.shrink_tendsto line 184
23. theorem OAI.HyperbolicObstruction.TangentCone.shrink_weight line 189
24. def OAI.HyperbolicObstruction.TangentCone.approxMid line 196
25. def OAI.HyperbolicObstruction.TangentCone.approxDist line 200
26. theorem OAI.HyperbolicObstruction.TangentCone.approxDist_tendsto line 203
27. theorem OAI.HyperbolicObstruction.TangentCone.approxMid_bound line 208
28. theorem OAI.HyperbolicObstruction.TangentCone.quadrilateral line 225
29. theorem OAI.HyperbolicObstruction.TangentCone.represented_midpoint_limit line 236
30. theorem OAI.HyperbolicObstruction.TangentCone.approxMid_cn line 246
31. theorem OAI.HyperbolicObstruction.TangentCone.exists_represented_mid line 263
32. def OAI.HyperbolicObstruction.TangentCone.representedMid line 282
33. theorem OAI.HyperbolicObstruction.TangentCone.representedMid_left line 285
34. theorem OAI.HyperbolicObstruction.TangentCone.representedMid_right line 289
35. theorem OAI.HyperbolicObstruction.TangentCone.representedMid_cn line 293
36. theorem OAI.HyperbolicObstruction.TangentCone.representedMid_swap line 297
37. theorem OAI.HyperbolicObstruction.TangentCone.representedMid_contraction line 305
38. theorem OAI.HyperbolicObstruction.TangentCone.representedMid_lipschitz line 316
39. def OAI.HyperbolicObstruction.TangentCone.coneMid line 330
40. theorem OAI.HyperbolicObstruction.TangentCone.continuous_coneMid line 333
41. theorem OAI.HyperbolicObstruction.TangentCone.coneMid_coe line 337
42. theorem OAI.HyperbolicObstruction.TangentCone.coneMid_left line 341
43. theorem OAI.HyperbolicObstruction.TangentCone.coneMid_right line 347
44. theorem OAI.HyperbolicObstruction.TangentCone.coneMid_cn line 353
45. theorem OAI.HyperbolicObstruction.strongly_convex_minimum line 370

    Source documentation

    The complete-space direct method for a squared-distance strongly convex functional. No local compactness is used.

    theorem strongly_convex_minimum {Y : Type*} [MetricSpace Y] [CompleteSpace Y] [Nonempty Y]
        (M : Y → Y → Y) (f : Y → ℝ) (hf : Continuous f)
        (hb : BddBelow (Set.range f))
        (hc : ∀ x y, f (M x y) ≤ (f x + f y) / 2 - dist x y ^ 2 / 4) :
        ∃ p, ∀ z, f p ≤ f z := by
    …

46. theorem OAI.HyperbolicObstruction.strongly_convex_variance line 400

    Source documentation

    Iterating midpoints toward a minimizer sharpens the one-step midpoint inequality to the exact variance inequality.

    theorem strongly_convex_variance {Y : Type*} [MetricSpace Y]
        (M : Y → Y → Y) (hM : ∀ x y, dist x (M x y) = dist x y / 2)
        (f : Y → ℝ)
        (hc : ∀ x y, f (M x y) ≤ (f x + f y) / 2 - dist x y ^ 2 / 4)
        (p : Y) (hp : ∀ z, f p ≤ f z) (z : Y) : f p + dist p z ^ 2 ≤ f z := by
    …

47. theorem OAI.HyperbolicObstruction.catZero_of_midpoints line 441

    Source documentation

    Full CAT(0) comparison from complete CN midpoints. The division point is constructed by minimizing a weighted squared-distance functional.

    theorem catZero_of_midpoints {Y : Type*} [MetricSpace Y] [CompleteSpace Y]
        (M : Y → Y → Y)
        (hM : ∀ x y, dist x (M x y) = dist x y / 2)
        (hCN : ∀ x y z, dist z (M x y) ^ 2 ≤
          (dist z x ^ 2 + dist z y ^ 2) / 2 - dist x y ^ 2 / 4) : CATZero Y := by
    …

    Mentions: OAI.HyperbolicObstruction.CATZero