RealShadowCartan.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.PolycyclicRecognition.weightImaginaryAction_apply_cartan line 16
Source documentation
Every imaginary Cartan derivation annihilates the whole Cartan algebra.
```
theorem weightImaginaryAction_apply_cartan (x : L) (h : H) :
    T.weightImaginaryAction H x h = 0 :=
…
```
def OAI.PolycyclicRecognition.realShadowCartanHom line 21
Source documentation
The Cartan factor retains its original Lie bracket.
```
def realShadowCartanHom : H →ₗ⁅ℝ⁆ CartanRealShadow T H where
…
```
Mentions: OAI.PolycyclicRecognition.CartanRealShadow
theorem OAI.PolycyclicRecognition.realShadowCartanHom_apply line 31
theorem OAI.PolycyclicRecognition.realShadowAdjoint_cartan line 36
Source documentation
For a Cartan parameter, the modified adjoint is exactly the original adjoint minus its imaginary semisimple part, on the entire vector space.
```
theorem realShadowAdjoint_cartan (h : H) (x : L) :
    realShadowAdjoint T H h x = ⁅(h : L),x⁆ - realImaginaryOperator L H h x := by
…
```
Mentions: OAI.PolycyclicRecognition.realShadowAdjoint, OAI.PolycyclicRecognition.realImaginaryOperator
theorem OAI.PolycyclicRecognition.realImaginaryOperator_commutes_ad line 42
Source documentation
The two operators whose exponentials occur in the rotational correction commute.
```
theorem realImaginaryOperator_commutes_ad (h : H) :
    Commute (realImaginaryOperator L H h) (ad ℝ L (h : L)) := by
…
```
Mentions: OAI.PolycyclicRecognition.realImaginaryOperator