RealShadowSplit.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Real triangularizability of the modified Lie algebra

def OAI.PolycyclicRecognition.realShadowAdjoint line 17
theorem OAI.PolycyclicRecognition.realShadowAdjoint_apply line 22
theorem OAI.PolycyclicRecognition.realShadowAdjoint_weight line 27
theorem OAI.PolycyclicRecognition.realShadowAdjoint_eq_on_kernel line 31
theorem OAI.PolycyclicRecognition.realShadowAdjoint_mul line 37
theorem OAI.PolycyclicRecognition.realShadowAdjoint_split_annihilator line 45
Source documentation
The extra correction in the actual adjoint action vanishes on its image. Thus one extra zero root transfers the real annihilator to that adjoint.
```
theorem realShadowAdjoint_split_annihilator (x : L) :
    ∃ S : Finset ℝ,
      Polynomial.aeval (realShadowAdjoint T H x)
        ((∏ a ∈ S, (Polynomial.X - Polynomial.C a)) ^ (n+1)) = 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.realShadowAdjoint
theorem OAI.PolycyclicRecognition.realShadowAdjoint_conjugate line 69
theorem OAI.PolycyclicRecognition.cartanRealShadow_isTriangularizable line 80
Source documentation
Every actual adjoint operator of the real shadow splits over the reals.
```
theorem cartanRealShadow_isTriangularizable :
    LieModule.IsTriangularizable ℝ (CartanRealShadow T H) (CartanRealShadow T H) where
…
```
Mentions: OAI.PolycyclicRecognition.CartanRealShadow
theorem OAI.PolycyclicRecognition.nonempty_cartanRealShadow_triangularAdjoint line 90
Source documentation
A genuine simultaneous real upper triangular adjoint basis.
```
theorem nonempty_cartanRealShadow_triangularAdjoint :
    ∃ m : ℕ, Nonempty (TriangularAdjoint (CartanRealShadow T H) m) := by
…
```
Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.CartanRealShadow