Documentation

LeanPool.Stafford38.AlgebraicAnalysis.CommutatorRiccati

Inverse-Euler/Riccati commutator identities #

This module contains the purely ring-theoretic identities behind the inverse-Euler calculation. No Weyl presentation, filtration, module, or application-specific hypothesis is assumed.

source
def AlgebraicAnalysis.InverseEulerRiccati.commutator {A : Type u_1} [Ring A] (a b : A) :
A

Historical local name for the shared ring commutator.

Equations
Instances For
    source
    @[simp]
    theorem AlgebraicAnalysis.InverseEulerRiccati.commutator_eq_shared {A : Type u_1} [Ring A] (a b : A) :
    commutator a b = ringCommutator a b
    source
    def AlgebraicAnalysis.InverseEulerRiccati.adIterate {A : Type u_1} [Ring A] (p : A) :
    ℕ → A → A

    Iterated commutation by a fixed element.

    Equations
    Instances For
      source
      theorem AlgebraicAnalysis.InverseEulerRiccati.inverse_riccati {A : Type u_1} [Ring A] (P X T : A) (hPX : P * X - X * P = -1) (hXT : X * T = 1) (hTX : T * X = 1) :
      P * T - T * P = T * T

      Inverting the relation P*X-X*P=-1 produces the Riccati identity.

      source
      theorem AlgebraicAnalysis.InverseEulerRiccati.euler_commutator {A : Type u_1} [Ring A] (P X T : A) (hPX : P * X - X * P = -1) (hXT : X * T = 1) (hTX : T * X = 1) :
      P * X * T - T * (P * X) = T

      The Euler element H = P*X has commutator T.

      source
      theorem AlgebraicAnalysis.InverseEulerRiccati.iterated_commutator {A : Type u_1} [Ring A] (P X T : A) (hPX : P * X - X * P = -1) (hXT : X * T = 1) (hTX : T * X = 1) (n : ℕ) :
      adIterate P n T = ↑n.factorial * T ^ (n + 1)

      The iterated commutator is the factorial Riccati tower.