OAI/GroupTheory/PolycyclicRecognition/Analysis/NilpotentWordMetric.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.dist_generatorGroupWord_le line 19

   Source documentation

   A word of bounded length and bounded letters has the corresponding metric bound in every group with a left invariant metric.

   theorem dist_generatorGroupWord_le
       {I L G : Type*} [SMul ℝ L] [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G]
       (X : I → L) (Exp : L → G) (u : List (I × ℝ)) {B D : ℝ}
       (hu : ∀ z ∈ u, |z.2| ≤ B)
       (hstep : ∀ i t, |t| ≤ B → dist 1 (Exp (t • X i)) ≤ D) :
       dist 1 (generatorGroupWord X Exp u) ≤ (u.length : ℝ) * D := by
   …

   Mentions: OAI.PolycyclicRecognition.generatorGroupWord

2. theorem OAI.PolycyclicRecognition.exists_unit_weight_chart_metric_bound line 45

   Source documentation

   Uniform generator-word bounds imply linear metric growth on every fixed-radius unit-weight chart. Only continuity of the generating flows is required from the metric; no geodesic or scaling estimate is assumed.

   theorem exists_unit_weight_chart_metric_bound
       {I L G : Type*} [Fintype I] [DecidableEq I]
       [LieRing L] [LieAlgebra ℝ L] [FiniteDimensional ℝ L]
       [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G]
       {A : Type*} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A]
       (X : I → L) {k c : ℕ} (hk : lowerCentralSeries ℝ L L k = ⊥)
       (hletters : ∀ i : I, FreeMagma.of i ∈ boundedBracketWords k)
       (b₀ : Basis (Fin (finrank ℝ L)) ℝ L)
       (Exp : L → G) (hinj : Function.Injective Exp)
       (hzero : Exp 0 = 1) (hneg : ∀ x, Exp (-x) = (Exp x)⁻¹)
       (hadd : ∀ x (s t : ℝ), Exp ((s + t) • x) = Exp (s • x) * Exp (t • x))
       (hcont : ∀ i, Continuous (fun t : ℝ => Exp (t • X i)))
   …

   Mentions: OAI.PolycyclicRecognition.boundedBracketWords