NilpotentNegativePaths.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Negative-height paths in the nilpotent Cartan factor

theorem OAI.PolycyclicRecognition.exists_nilpotent_negative_paths line 21

Source documentation

A fixed Cartan displacement can be moved along a negative ray by paths in a linear ball. Their coarse speeds grow only polynomially.

theorem exists_nilpotent_negative_paths
    (κ : D →* G) (hκ : Continuous κ)
    (dynkin : NilpotentDynkinExpansionInput E D)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) D → D) (hExp : IsGroupExponential Exp)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) D ≃ₜ D) (hchart : ∀ x, chart x = Exp x)
    {c : ℕ} (hc : lowerCentralSeries ℝ (GroupLieAlgebra (𝓘(ℝ, E)) D)
      (GroupLieAlgebra (𝓘(ℝ, E)) D) c = ⊥)
    {m : ℕ} (b : Basis (Fin m) ℝ (GroupLieAlgebra (𝓘(ℝ, E)) D))
    (η : G →* Multiplicative ℝ)
    (ℓ : GroupLieAlgebra (𝓘(ℝ, E)) D →ₗ[ℝ] ℝ)
    (hη : ∀ w, (η (κ (Exp w))).toAdd = ℓ w)
    (u v : GroupLieAlgebra (𝓘(ℝ, E)) D) (hv : ℓ v < 0) :
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput