InvariantMetrization.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

A compatible left-invariant metric

Take the supremum of the bounded metric over left translations. The left uniformity makes this supremum compatible with the original topology. This supplies the metrization step in the proper chain-metric construction.

def OAI.PolycyclicRecognition.leftInvariantDistance line 23
Source documentation
The bounded supremum over all left translations of a given metric.
```
def leftInvariantDistance (x y : G) : ℝ :=
…
```
theorem OAI.PolycyclicRecognition.translateDistance_bdd line 26
theorem OAI.PolycyclicRecognition.leftInvariantDistance_le_one line 30
theorem OAI.PolycyclicRecognition.min_dist_le_leftInvariantDistance line 33
theorem OAI.PolycyclicRecognition.leftInvariantDistance_self line 37
theorem OAI.PolycyclicRecognition.leftInvariantDistance_comm line 40
theorem OAI.PolycyclicRecognition.min_one_add_le line 44
theorem OAI.PolycyclicRecognition.leftInvariantDistance_triangle line 54
theorem OAI.PolycyclicRecognition.leftInvariantDistance_mul_left line 63
theorem OAI.PolycyclicRecognition.leftTranslations_uniform_control line 78
Source documentation
All left translations are equicontinuous for a metric inducing the left uniformity.
```
theorem leftTranslations_uniform_control {ε : ℝ} (hε : 0 < ε) :
    ∃ δ > 0, ∀ x y : G, dist x y < δ → ∀ g : G, dist (g * x) (g * y) < ε := by
…
```
theorem OAI.PolycyclicRecognition.leftInvariantDistance_topology line 94
def OAI.PolycyclicRecognition.leftInvariantMetric line 122
Source documentation
The left-invariant metric with exactly the original topology.
```
def leftInvariantMetric : MetricSpace G :=
…
```
theorem OAI.PolycyclicRecognition.leftInvariantMetric_isometric line 132

theorem OAI.PolycyclicRecognition.exists_bounded_leftInvariant_metric line 146

Source documentation

Every first-countable Hausdorff topological group has a bounded, compatible left-invariant metric.

theorem exists_bounded_leftInvariant_metric
    {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    [FirstCountableTopology H] [T2Space H] :
    ∃ m : MetricSpace H,
      m.toUniformSpace.toTopologicalSpace = ‹TopologicalSpace H› ∧
      (letI := m; IsIsometricSMul H H) ∧
…