ConjugationFlow.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The actual conjugation flow of a matrix exponential

Left and right multiplication give the exponential formula for the adjoint operator. This supplies the conjugation identity used by root distortion.

def OAI.PolycyclicRecognition.leftRegular line 18
def OAI.PolycyclicRecognition.rightRegular line 26
theorem OAI.PolycyclicRecognition.continuous_leftRegular line 34
theorem OAI.PolycyclicRecognition.continuous_rightRegular line 37
def OAI.PolycyclicRecognition.adjointOperator line 40
theorem OAI.PolycyclicRecognition.adjointOperator_apply line 43
theorem OAI.PolycyclicRecognition.exp_adjointOperator_apply line 49
Source documentation
Exponentiating the commutator operator gives actual conjugation.
```
theorem exp_adjointOperator_apply (x y : A) :
    (NormedSpace.exp (adjointOperator x)) y =
      NormedSpace.exp x * y * NormedSpace.exp (-x) := by
…
```
Mentions: OAI.PolycyclicRecognition.adjointOperator
theorem OAI.PolycyclicRecognition.exp_smul_adjointOperator_apply line 69

theorem OAI.PolycyclicRecognition.exp_intertwine_apply line 79

Source documentation

A continuous linear intertwiner also intertwines the actual analytic operator exponentials, so restricted root actions agree with ambient ones.

theorem exp_intertwine_apply
    {V U : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V]
    [NormedAddCommGroup U] [NormedSpace ℝ U] [CompleteSpace U]
    (f : V →L[ℝ] U) (S : V →L[ℝ] V) (T : U →L[ℝ] U)
    (hf : ∀ v, f (S v) = T (f v)) (v : V) :
    f ((NormedSpace.exp S) v) = (NormedSpace.exp T) (f v) := by
…