OAI/GroupTheory/PolycyclicRecognition/Geometry/RescaledFlowLipschitz.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.rescaled_profile_flow_dist_le line 15
2. theorem OAI.PolycyclicRecognition.lipschitz_supported_rescaled_flow line 51

   Source documentation

   All supported weak limits of the actual rescaled profiles are Lipschitz along the graded flow. The constant is independent of the base point and of the supported profile.

   theorem lipschitz_supported_rescaled_flow
       {L D G W A : Type*} [LieRing L] [LieAlgebra ℝ L] [Group D]
       [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G]
       [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace A]
       {n c : ℕ} (Exp : L → D) (κ : D →* G) (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)
       (a : DynkinCoefficients c 2)
       (hm : ∀ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y)
       (v : L) (hv : ∀ j, b.repr v j ≠ 0 → 1 ≤ cost j)
       (hd : Continuous (fun t : ℝ => κ (Exp (t • v))))
       (hd0 : κ (Exp ((0 : ℝ) • v)) = 1)
   …

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