CartanResidualDerivation.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

The actual nilpotent residual derivation

Subtracting the scalar weight derivation from the Cartan adjoint action gives one globally nilpotent derivation, not merely separate nilpotent operators on its root spaces. Its finite exponential is therefore an actual Lie automorphism.

def OAI.PolycyclicRecognition.cartanScalarOperator line 26
Source documentation
The scalar part of the Cartan adjoint operator on the generalized-root sum, before exponentiation.
```
def cartanScalarOperator (h : H) : L →ₗ[ℝ] L := by
…
```
theorem OAI.PolycyclicRecognition.cartanScalarOperator_apply_root line 32
theorem OAI.PolycyclicRecognition.cartanScalarOperator_apply_genWeight line 45
theorem OAI.PolycyclicRecognition.cartanScalarOperator_leibniz line 54
Source documentation
Weight addition in brackets is precisely the derivation identity for the scalar part.
```
theorem cartanScalarOperator_leibniz (h : H) (x y : L) :
    cartanScalarOperator T H h ⁅x, y⁆ =
      ⁅x, cartanScalarOperator T H h y⁆ + ⁅cartanScalarOperator T H h x, y⁆ := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanScalarOperator
def OAI.PolycyclicRecognition.cartanScalarDerivation line 76
Source documentation
The scalar part as a genuine derivation of the ambient Lie algebra.
```
def cartanScalarDerivation (h : H) : LieDerivation ℝ L L where
…
```
def OAI.PolycyclicRecognition.cartanResidualDerivation line 84
Source documentation
The globally defined residual action. The library's inner h sends x to [x,h], hence the minus sign.
```
def cartanResidualDerivation (h : H) : LieDerivation ℝ L L :=
…
```
theorem OAI.PolycyclicRecognition.cartanResidualDerivation_apply_root line 87
theorem OAI.PolycyclicRecognition.cartanResidualDerivation_root_mem line 93
theorem OAI.PolycyclicRecognition.cartanResidualDerivation_pow_root line 98
theorem OAI.PolycyclicRecognition.cartanResidualDerivation_pow_eq_zero line 114
Source documentation
The ambient dimension is a simultaneous nilpotence bound on every root.
```
theorem cartanResidualDerivation_pow_eq_zero (h : H) :
    (cartanResidualDerivation T H h).toLinearMap ^ finrank ℝ L = 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanResidualDerivation
def OAI.PolycyclicRecognition.cartanResidualAutomorphism line 133
Source documentation
The residual action exponentiates by a finite polynomial to an actual Lie automorphism.
```
def cartanResidualAutomorphism (h : H) : L ≃ₗ⁅ℝ⁆ L := by
…
```
theorem OAI.PolycyclicRecognition.cartanScalarOperator_mem_ideal line 139
Source documentation
The scalar derivation preserves the actual nilpotent Cartan ideal.
```
theorem cartanScalarOperator_mem_ideal (h : H) {x : L} (hx : x ∈ cartanRootIdeal H) :
    cartanScalarOperator T H h x ∈ cartanRootIdeal H := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.cartanScalarOperator
theorem OAI.PolycyclicRecognition.cartanResidualDerivation_mem_ideal line 169
Source documentation
Consequently the full residual derivation preserves the ideal.
```
theorem cartanResidualDerivation_mem_ideal (h : H) {x : L} (hx : x ∈ cartanRootIdeal H) :
    cartanResidualDerivation T H h x ∈ cartanRootIdeal H := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.cartanResidualDerivation
def OAI.PolycyclicRecognition.cartanIdealResidualDerivation line 177
Source documentation
Restrict the residual derivation before taking its finite exponential.
```
def cartanIdealResidualDerivation (h : H) :
    LieDerivation ℝ (cartanRootIdeal H) (cartanRootIdeal H) where
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal
theorem OAI.PolycyclicRecognition.cartanIdealResidualDerivation_pow_coe line 187
theorem OAI.PolycyclicRecognition.cartanIdealResidualDerivation_pow_eq_zero line 196
def OAI.PolycyclicRecognition.cartanIdealResidualAutomorphism line 206
Source documentation
The residual automorphism of the nilpotent factor used in box estimates.
```
def cartanIdealResidualAutomorphism (h : H) : cartanRootIdeal H ≃ₗ⁅ℝ⁆ cartanRootIdeal H := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal