OAI/GroupTheory/PolycyclicRecognition/Analysis/RescaledBoxTranslation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Small translations of actual rescaled nilpotent boxes

The coordinate basis can vary without convergence. Bounded normalized brackets and a vanishing translation coordinate suffice for the fixed cube. All measure preservation is proved from the published exponential Haar input.

  1. theorem OAI.PolycyclicRecognition.actual_rescaled_cell_translation_tendsto_zero line 22

    Source documentation

    The actual normalized cells are asymptotically unchanged by right translations whose normalized logarithms tend to zero.

    theorem actual_rescaled_cell_translation_tendsto_zero
    {E G ΞΉ : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] [TopologicalSpace G] [ChartedSpace E G] [Group G]
    [LieGroup (π“˜(ℝ, E)) ⊀ G] [T2Space G] [SimplyConnectedSpace G]
    [MeasurableSpace G] [BorelSpace G]
    (haar : NilpotentExponentialHaarInput E G)
    (Exp : GroupLieAlgebra (π“˜(ℝ, E)) G β†’ G) (hExp : IsGroupExponential Exp)
    (hnil : LieRing.IsNilpotent (GroupLieAlgebra (π“˜(ℝ, E)) G))
    {n c : β„•} (b : ΞΉ β†’ Basis (Fin n) ℝ (GroupLieAlgebra (π“˜(ℝ, E)) G))
    (a : DynkinCoefficients c 2)
    (hm : βˆ€ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y)
    {C : ℝ} (hbound : βˆ€ i, β€–basisBracket (b i)β€– ≀ C)
…

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