OAI/GroupTheory/PolycyclicRecognition/Analysis/CompatibleMetricComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.ProperChainMetric.compare line 13

   Source documentation

   Any two proper, compatible, left-invariant chain metrics on the same group have affine comparison bounds. This is applied to the fixed metric and the chosen Riemannian metric, with the identity map on the group.

   theorem ProperChainMetric.compare
       {G : Type} [Group G] [TopologicalSpace G]
       (d₁ d₂ : ProperChainMetric G) :
       ∃ K C : ℝ, 0 ≤ K ∧ 0 ≤ C ∧ ∀ x y : G,
         @dist G d₂.compatibleMetric.toPseudoMetricSpace.toDist x y ≤
           K * @dist G d₁.compatibleMetric.toPseudoMetricSpace.toDist x y + C := by
   …

   Mentions: OAI.PolycyclicRecognition.ProperChainMetric