ComplexRotationDerivation.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The infinitesimal imaginary Cartan action

The infinitesimal compact action is a genuine Lie derivation. Subtracting it from the original adjoint action removes exactly the imaginary weights.

def OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator line 20
Source documentation
Imaginary semisimple part of a Cartan adjoint operator.
```
def imaginaryOperator (h : H) : L →ₗ[ℂ] L :=
…
```
theorem OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator_apply line 23
theorem OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator_apply_genWeight line 28
theorem OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator_lie line 37
Source documentation
The root-bracket rule makes the imaginary semisimple part a derivation.
```
theorem imaginaryOperator_lie (h : H) (x y : L) :
    imaginaryOperator H h ⁅x,y⁆ =
      ⁅imaginaryOperator H h x,y⁆ + ⁅x,imaginaryOperator H h y⁆ := by
…
```
Mentions: OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator
def OAI.PolycyclicRecognition.ComplexCartan.imaginaryDerivation line 58
Source documentation
The infinitesimal rotation as a bundled derivation.
```
def imaginaryDerivation (h : H) : LieDerivation ℂ L L where
…
```
theorem OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator_add line 64
theorem OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator_zero line 74
theorem OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator_real_smul line 83
Source documentation
Dependence on the Cartan parameter is real linear.
```
theorem imaginaryOperator_real_smul (r : ℝ) (h : H) (x : L) :
    imaginaryOperator H (r • h) x = r • imaginaryOperator H h x := by
…
```
Mentions: OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator
theorem OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator_commute line 94
Source documentation
The imaginary operators commute, including on generalized weight spaces.
```
theorem imaginaryOperator_commute (h k : H) (x : L) :
    imaginaryOperator H h (imaginaryOperator H k x) =
      imaginaryOperator H k (imaginaryOperator H h x) := by
…
```
Mentions: OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator
theorem OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator_cartan line 107
Source documentation
The zero-weight Cartan algebra is fixed infinitesimally.
```
theorem imaginaryOperator_cartan (h k : H) : imaginaryOperator H h k = 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator