OAI/GroupTheory/PolycyclicRecognition/Analysis/AllScaleProfileEquicontinuity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.continuous_scaled_basis_coordinates line 14
2. theorem OAI.PolycyclicRecognition.continuous_mapped_scaled_basis_coordinates line 27
3. theorem OAI.PolycyclicRecognition.equicontinuous_all_scale_profiles line 43

   Source documentation

   Uniformity of the actual metric error over all nonnegative real scales. Compact initial scale intervals and the asymptotic chart estimate give a single modulus, independent of the eventual sequence.

   theorem equicontinuous_all_scale_profiles
       {L G W P : Type*} [LieRing L] [LieAlgebra ℝ L]
       [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G]
       [NormedAddCommGroup W] [NormedSpace ℝ W] {n c : ℕ}
       (b : Basis (Fin n) ℝ L) (cost : Fin n → ℝ)
       (hweight : ∀ i j k, b.repr ⁅b i, b j⁆ k ≠ 0 → cost i + cost j ≤ cost k)
       (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))
       (a : DynkinCoefficients c 2)
       (hm : ∀ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y)
       {C : ℝ} (hC : 0 ≤ C)
   …

   Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial