CoordinateConjugation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Conjugation identities persist under coordinate limits

The exponential of the coordinate adjoint is the genuine logarithmic conjugation map. This identity is closed in the bracket parameter and will identify the columns of the limiting generator endpoint map.

def OAI.PolycyclicRecognition.ExponentialConjugationLaw line 21
Source documentation
The usual adjoint-exponential identity written entirely in fixed coordinates.
```
def ExponentialConjugationLaw (m : V → V → V) (B : V →L[ℝ] V →L[ℝ] V) : Prop :=
…
```
theorem OAI.PolycyclicRecognition.isClosed_exponentialConjugationLaw line 26
Source documentation
The logarithmic conjugation identity is a closed condition.
```
theorem isClosed_exponentialConjugationLaw {c : ℕ} (a : DynkinCoefficients c 2) :
    IsClosed {B : V →L[ℝ] V →L[ℝ] V |
      ExponentialConjugationLaw (dynkinProduct a B) B} := by
…
```
Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.ExponentialConjugationLaw, OAI.PolycyclicRecognition.dynkinProduct

theorem OAI.PolycyclicRecognition.basis_exp_adjoint line 56

Source documentation

Coordinate change intertwines actual adjoint exponentials.

theorem basis_exp_adjoint {n : ℕ} (b : Module.Basis (Fin n) ℝ L)
    (x y : L) (t : ℝ) :
    b.equivFun (NormedSpace.exp (t • continuousAd x) y) =
      NormedSpace.exp (t • basisBracket b (b.equivFun x)) (b.equivFun y) := by
…

Mentions: OAI.PolycyclicRecognition.continuousAd, OAI.PolycyclicRecognition.basisBracket

theorem OAI.PolycyclicRecognition.basis_exponentialConjugationLaw line 73

Source documentation

The representation-derived conjugation formula transports to every coordinate basis with the same binary Dynkin coefficients.

theorem basis_exponentialConjugationLaw {n c : ℕ} (b : Module.Basis (Fin n) ℝ L)
    (Exp : L → G) (hinj : Function.Injective Exp)
    (hneg : ∀ x, Exp (-x) = (Exp x)⁻¹)
    (a : DynkinCoefficients c 2)
    (hm : ∀ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y)
    (j : L →ₗ⁅ℝ⁆ A) (ρ : G →* Aˣ) (hρ : Function.Injective ρ)
    (hmatch : ∀ x, ρ (Exp x) = algebraExpUnit (j x)) :
    ExponentialConjugationLaw (dynkinProduct a (basisBracket b)) (basisBracket b) := by
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial, OAI.PolycyclicRecognition.algebraExpUnit, OAI.PolycyclicRecognition.ExponentialConjugationLaw, OAI.PolycyclicRecognition.dynkinProduct, OAI.PolycyclicRecognition.basisBracket