NilpotentConjugationCoordinates.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Polynomial speed of a conjugated nilpotent one-parameter subgroup

theorem OAI.PolycyclicRecognition.exists_nilpotent_conjugation_coordinate_bound line 20

Source documentation

In a nilpotent group, conjugating a fixed exponential line by a ray costs a polynomial in the ray parameter, retaining its linear time factor.

theorem exists_nilpotent_conjugation_coordinate_bound
    (dynkin : NilpotentDynkinExpansionInput E G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G) (hchart : ∀ x, chart x = Exp x)
    {c : ℕ} (hc : lowerCentralSeries ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G)
      (GroupLieAlgebra (𝓘(ℝ, E)) G) c = ⊥)
    (b : Basis J ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G))
    (u v : GroupLieAlgebra (𝓘(ℝ, E)) G) :
    ∃ A : ℝ, 0 ≤ A ∧ ∀ (n : ℕ) (s : ℝ), |s| ≤ 1 →
      ‖b.equivFun (chart.symm
        (Exp (-(n : ℝ) • v) * Exp (s • u) * Exp ((n : ℝ) • v)))‖ ≤
          A * (1 + n) ^ c * |s| := by
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput