CartanResidualExponential.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Polynomial formulas for the residual Cartan automorphism

The global residual Lie automorphism agrees with the analytic exponential of the nilpotent residual operator on every root. This connects its algebraic construction to the root-space estimates.

theorem OAI.PolycyclicRecognition.cartanIdealResidualAutomorphism_apply line 26
Source documentation
The residual automorphism is an explicit finite real Lie polynomial.
```
theorem cartanIdealResidualAutomorphism_apply (h : H) (x : cartanRootIdeal H) :
    cartanIdealResidualAutomorphism T H h x =
      ∑ k ∈ Finset.range (finrank ℝ L), ((k.factorial : ℝ)⁻¹) •
        ((cartanIdealResidualDerivation T H h).toLinearMap ^ k) x := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.cartanIdealResidualAutomorphism, OAI.PolycyclicRecognition.cartanIdealResidualDerivation
theorem OAI.PolycyclicRecognition.cartanIdealResidualDerivation_pow_root_mem line 40
Source documentation
Every residual power preserves its actual generalized root space.
```
theorem cartanIdealResidualDerivation_pow_root_mem (h : H) (χ : Weight ℝ H L)
    (k : ℕ) (x : cartanRootIdeal H) (hx : (x : L) ∈ rootSpace H χ) :
    (((cartanIdealResidualDerivation T H h).toLinearMap ^ k) x : L) ∈ rootSpace H χ := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.cartanIdealResidualDerivation
theorem OAI.PolycyclicRecognition.cartanIdealResidualAutomorphism_root_mem line 52
Source documentation
The finite exponential preserves each root space.
```
theorem cartanIdealResidualAutomorphism_root_mem (h : H) (χ : Weight ℝ H L)
    (x : cartanRootIdeal H) (hx : (x : L) ∈ rootSpace H χ) :
    (cartanIdealResidualAutomorphism T H h x : L) ∈ rootSpace H χ := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.cartanIdealResidualAutomorphism