OAI/Geometry/HyperbolicGroups/MetricProduct.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.MetricProduct.dist_sq line 45
2. def OAI.HyperbolicObstruction.MetricProduct.segment line 53
3. lemma OAI.HyperbolicObstruction.MetricProduct.segment_apply line 57
4. lemma OAI.HyperbolicObstruction.MetricProduct.segment_zero line 61
5. lemma OAI.HyperbolicObstruction.MetricProduct.segment_one line 66
6. lemma OAI.HyperbolicObstruction.MetricProduct.segment_dist line 70
7. lemma OAI.HyperbolicObstruction.MetricProduct.segment_cn line 81
8. theorem OAI.HyperbolicObstruction.MetricProduct.catZero line 89

   Source documentation

   Finite L2 products preserve CAT(0), by summing the coordinate CN comparisons.

   theorem catZero : CATZero (PiLp 2 X) := by
   …

   Mentions: OAI.HyperbolicObstruction.CATZero

9. lemma OAI.HyperbolicObstruction.MetricProduct.apply_segment line 94
10. def OAI.HyperbolicObstruction.MeanProduct.factor line 116
11. lemma OAI.HyperbolicObstruction.MeanProduct.factor_pos line 118
12. lemma OAI.HyperbolicObstruction.MeanProduct.factor_sq line 122
13. abbrev OAI.HyperbolicObstruction.MeanProduct.Space line 127
14. def OAI.HyperbolicObstruction.MeanProduct.ofFn line 129
15. def OAI.HyperbolicObstruction.MeanProduct.apply line 133
16. lemma OAI.HyperbolicObstruction.MeanProduct.ofFn_apply line 136
17. lemma OAI.HyperbolicObstruction.MeanProduct.dist_sq line 138
18. lemma OAI.HyperbolicObstruction.MeanProduct.dist_le_of_forall line 143
19. theorem OAI.HyperbolicObstruction.MeanProduct.catZero line 156
20. lemma OAI.HyperbolicObstruction.MeanProduct.apply_segment line 159
21. structure OAI.HyperbolicObstruction.MetricLimit.Bounded line 178

    Source documentation

    Uniformly bounded pointed sections of the actual varying action spaces.

    @[ext] structure Bounded (U : Ultrafilter ℕ) (X : ℕ → Type u)
        [∀ n, MetricSpace (X n)] (o : ∀ n, X n) where
    …

22. lemma OAI.HyperbolicObstruction.MetricLimit.bounded_dist line 185
23. def OAI.HyperbolicObstruction.MetricLimit.preDist line 194

    Source documentation

    Real ultrafilter distance; boundedness proves convergence rather than assuming existence of a limiting metric.

    def preDist (x y : Bounded U X o) : ℝ :=
    …

    Mentions: OAI.HyperbolicObstruction.MetricLimit.Bounded

24. lemma OAI.HyperbolicObstruction.MetricLimit.tendsto_dist line 197
25. instance OAI.HyperbolicObstruction.MetricLimit.(instance at line 208) line 208
26. abbrev OAI.HyperbolicObstruction.MetricLimit.Space line 220

    Source documentation

    The separated metric ultralimit. Completeness is not needed for the finite obstruction; all segment and CN comparisons are established below.

    abbrev Space := SeparationQuotient (Bounded U X o)

    Mentions: OAI.HyperbolicObstruction.MetricLimit.Bounded

27. def OAI.HyperbolicObstruction.MetricLimit.point line 222
28. lemma OAI.HyperbolicObstruction.MetricLimit.tendsto_point_dist line 224
29. def OAI.HyperbolicObstruction.MetricLimit.segment line 232

    Source documentation

    Coordinate segments are clamped outside the parameter interval, so the boundedness obligation never relies on the arbitrary extension of a segment.

    def segment (x y : Bounded U X o) (t : ℝ) : Bounded U X o :=
    …

    Mentions: OAI.HyperbolicObstruction.MetricLimit.Bounded

30. lemma OAI.HyperbolicObstruction.MetricLimit.segment_val line 251
31. lemma OAI.HyperbolicObstruction.MetricLimit.segment_zero line 255
32. lemma OAI.HyperbolicObstruction.MetricLimit.segment_one line 261
33. lemma OAI.HyperbolicObstruction.MetricLimit.segment_dist line 267
34. lemma OAI.HyperbolicObstruction.MetricLimit.segment_cn line 276
35. theorem OAI.HyperbolicObstruction.MetricLimit.catZero line 294

    Source documentation

    CAT(0) comparison survives this metric ultralimit, proved directly from CN and the convergence of every bounded pair of coordinate sections.

    theorem catZero : CATZero (Space (U := U) (X := X) (o := o)) := by
    …

    Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.MetricLimit.Space

36. lemma OAI.HyperbolicObstruction.MetricLimit.point_segment line 311

    Source documentation

    Uniqueness identifies actual chosen limit segments, not just their endpoints.

    lemma point_segment (x y : Bounded U X o) {t : ℝ} (ht : t ∈ Set.Icc (0 : ℝ) 1) :
        point (segment h x y t) = CATZero.segment (catZero h) (point x) (point y) t := by
    …

    Mentions: OAI.HyperbolicObstruction.MetricLimit.Bounded, OAI.HyperbolicObstruction.MetricLimit.point, OAI.HyperbolicObstruction.MetricLimit.segment, OAI.HyperbolicObstruction.CATZero.segment, OAI.HyperbolicObstruction.MetricLimit.catZero

37. theorem OAI.HyperbolicObstruction.le_of_tendsto_upper_error line 330

    Source documentation

    A one-sided error estimate suffices; the action-dependent errors need not converge, and no illicit interchange of angle and ultralimit is used.

    theorem le_of_tendsto_upper_error {α : Type*} {l : Filter α} [l.NeBot]
        {f g e : α → ℝ} {a b : ℝ} (hf : Tendsto f l (𝓝 a)) (hg : Tendsto g l (𝓝 b))
        (he : ∀ ε : ℝ, 0 < ε → ∀ᶠ n in l, e n < ε)
        (hfg : ∀ᶠ n in l, f n ≤ g n + e n) : a ≤ b := by
    …

38. lemma OAI.HyperbolicObstruction.MetricLimit.tendsto_point_dist_sq line 347
39. lemma OAI.HyperbolicObstruction.MetricLimit.dist_sq_eq_of_tendsto line 351
40. lemma OAI.HyperbolicObstruction.MetricLimit.lower_of_eventually line 356
41. def OAI.HyperbolicObstruction.MetricScale.isometryEquiv line 376
42. def OAI.HyperbolicObstruction.MetricScale.action line 385
43. lemma OAI.HyperbolicObstruction.MetricScale.action_val line 394
44. theorem OAI.HyperbolicObstruction.IsometricAction.displacement_inv line 402
45. theorem OAI.HyperbolicObstruction.IsometricAction.displacement_mul_le line 411
46. theorem OAI.HyperbolicObstruction.IsometricAction.displacement_prod_le line 417
47. theorem OAI.HyperbolicObstruction.IsometricAction.six_letter_displacement_bound line 425
48. theorem OAI.HyperbolicObstruction.IsometricAction.normalized_minimum line 454

    Source documentation

    Exact normalized displacement minimum obtained by rescaling the actual action.

    theorem normalized_minimum [Nonempty X] [ProperSpace X] [Infinite G]
        {ι : Type*} [Fintype ι] [Nonempty ι] (A : GeometricAction G X) (letter : ι → G)
        (hgen : Subgroup.closure (Set.range letter) = ⊤) :
        ∃ r : ℝ, ∃ hr : 0 < r, ∃ o : MetricScale.Space r hr X,
          (𝔼 i, dist o (MetricScale.action A.act (letter i) o) ^ 2) = 1 ∧
          ∀ y : MetricScale.Space r hr X,
            (∑ i, dist o (MetricScale.action A.act (letter i) o) ^ 2) ≤
            ∑ i, dist y (MetricScale.action A.act (letter i) y) ^ 2 := by
    …

    Mentions: OAI.HyperbolicObstruction.GeometricAction, OAI.HyperbolicObstruction.MetricScale.Space, OAI.HyperbolicObstruction.MetricScale.action