OAI/GroupTheory/PolycyclicRecognition/Analysis/MinimizingMetricChains.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.linearMetricChains_of_minimizing_paths line 15

   Source documentation

   Sampling the chosen minimizing paths gives the concrete chain witnesses needed by the canonical-height and proper-homomorphism metric bridges.

   def linearMetricChains_of_minimizing_paths
       {G : Type*} [Group G] [MetricSpace G] [IsIsometricSMul G G]
       (hpath : ∀ g : G, ∃ γ : ℝ → G, γ 0 = 1 ∧ γ 1 = g ∧
         ∀ t ∈ Icc (0 : ℝ) 1, ∀ u ∈ Icc (0 : ℝ) 1,
           dist (γ t) (γ u) ≤ dist 1 g * |t - u|) :
       LinearMetricChains G := by
   …