MinimizingLieMetric.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The published minimizing metric on the connected Lie model

The sole input is the connected Lie-group specialization of J. M. Lee, Introduction to Riemannian Manifolds, second edition, GTM 176 (2018): Lemma 3.10(b), p. 68 constructs a left-invariant Riemannian metric; Problem 6-12(c), p. 188 gives completeness of homogeneous metrics; Corollary 6.21, p. 170 gives minimizing segments; Problem 6-14(a), p. 188 (or the compact exponential-ball argument in Lemma 6.18) gives properness. Only the resulting metric and normalized minimizing paths are retained. The large-scale chain property is proved here rather than included in the published hypothesis.

structure OAI.PolycyclicRecognition.ProperMinimizingMetric line 25
Source documentation
The metric consequences of a complete left-invariant Riemannian metric.
```
structure ProperMinimizingMetric (G : Type*) [Group G] [TopologicalSpace G] where
…
```
def OAI.PolycyclicRecognition.LieMinimizingMetricInput line 37
Source documentation
Precisely the metric specialization of the cited published results; there is no height, quasi-isometry, or recognition assertion in this input.
```
def LieMinimizingMetricInput : Prop :=
…
```
def OAI.PolycyclicRecognition.ProperMinimizingMetric.toProperChainMetric line 46
Source documentation
Sampling minimizing paths provides the chain structure for the existing proper-homomorphism and canonical-height metric comparisons.
```
def toProperChainMetric : ProperChainMetric G where
…
```
Mentions: OAI.PolycyclicRecognition.ProperChainMetric
theorem OAI.PolycyclicRecognition.ProperMinimizingMetric.minimizing_compatibleMetric line 56