CartanRealDiagonal.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Removing the imaginary Cartan eigenvalues on the original flag

theorem OAI.PolycyclicRecognition.ComplexCartan.semisimpleOperator_diagonal line 15
theorem OAI.PolycyclicRecognition.ComplexCartan.semisimpleOperator_diagonal_weight line 30
Source documentation
Each diagonal eigenvalue of the semisimple operator is one of its root-space eigenvalues, including when several roots have the same value.
```
theorem semisimpleOperator_diagonal_weight {n : ℕ} (b : Basis (Fin n) ℂ L) (h : H)
    (hh : (LinearMap.toMatrix b b (ad ℂ L (h : L))).IsUpperTriangular) (i : Fin n) :
    ∃ χ : Weight ℂ H L, LinearMap.toMatrix b b (semisimpleOperator H h) i i = χ h := by
…
```
Mentions: OAI.PolycyclicRecognition.ComplexCartan.semisimpleOperator

theorem OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator_diagonal line 62

Source documentation

Polynomial interpolation removes exactly the imaginary diagonal part.

theorem imaginaryOperator_diagonal {n : ℕ} (b : Basis (Fin n) ℂ L) (h : H)
    (hh : (LinearMap.toMatrix b b (ad ℂ L (h : L))).IsUpperTriangular) (i : Fin n) :
    LinearMap.toMatrix b b (imaginaryOperator H h) i i =
      imaginaryPart (LinearMap.toMatrix b b (ad ℂ L (h : L)) i i) := by
…

Mentions: OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator, OAI.PolycyclicRecognition.ComplexCartan.imaginaryPart

theorem OAI.PolycyclicRecognition.ComplexCartan.realPartOperator_diagonal_im line 85