AdjointExponentialRepresentation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Identifying the actual adjoint exponential through a faithful representation

def OAI.PolycyclicRecognition.adjointExponentialLinear line 24
Source documentation
The algebraic endomorphism underlying the analytic exponential of ad x. The auxiliary finite-dimensional norm is not part of the output.
```
def adjointExponentialLinear (x : L) : L →ₗ[ℝ] L :=
…
```
theorem OAI.PolycyclicRecognition.toMatrix_adjointExponentialLinear line 27
theorem OAI.PolycyclicRecognition.exp_adjointExponentialLinear line 45

theorem OAI.PolycyclicRecognition.conjugationDifferential_exp line 67

Source documentation

Faithful exponential compatibility identifies the actual tangent adjoint action with the algebraic adjoint exponential.

theorem conjugationDifferential_exp
    {Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G} (hExp : IsGroupExponential Exp)
    (j : GroupLieAlgebra (𝓘(ℝ, E)) G →ₗ⁅ℝ⁆ A) (ρ : G →* Aˣ)
    (hρ : Function.Injective ρ) (hρExp : ∀ x, ρ (Exp x) = algebraExpUnit (j x))
    (x : GroupLieAlgebra (𝓘(ℝ, E)) G) :
    (conjugationDifferentialHom (Exp x)).toLinearMap = adjointExponentialLinear x := by
…

Mentions: OAI.PolycyclicRecognition.algebraExpUnit, OAI.PolycyclicRecognition.conjugationDifferentialHom, OAI.PolycyclicRecognition.adjointExponentialLinear