ImaginaryOperatorPolynomial.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Polynomial interpolation on the finite set of Cartan eigenvalues realizes the imaginary part as a polynomial in the Jordan semisimple operator.

theorem OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator_polynomial line 23
Source documentation
Interpolation is on eigenvalues, so coincident weights cause no choice or distinctness assumption.
```
theorem imaginaryOperator_polynomial (h : H) :
    ∃ p : Polynomial ℂ, Polynomial.aeval (semisimpleOperator H h) p = imaginaryOperator H h := by
…
```
Mentions: OAI.PolycyclicRecognition.ComplexCartan.semisimpleOperator, OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator
theorem OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator_adjoin line 44
Source documentation
The imaginary part is a polynomial in the original Cartan adjoint operator, through its Jordan semisimple part.
```
theorem imaginaryOperator_adjoin (h : H) :
    imaginaryOperator H h ∈ Algebra.adjoin ℂ {ad ℂ L (h : L)} := by
…
```
Mentions: OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator
theorem OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator_upper line 58
Source documentation
The imaginary semisimple operator preserves the same upper triangular flag as the original adjoint action.
```
theorem imaginaryOperator_upper {n : ℕ} (b : Basis (Fin n) ℂ L) (h : H)
    (hh : (LinearMap.toMatrix b b (ad ℂ L (h : L))).IsUpperTriangular) :
    (LinearMap.toMatrix b b (imaginaryOperator H h)).IsUpperTriangular := by
…
```
Mentions: OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator