HaarPolynomialDerivation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Polynomial directional derivatives for left matrix multiplication.

abbrev OAI.InvariantIsing.MatrixPolynomial line 13
def OAI.InvariantIsing.matrixPolynomialDerivation line 16
Source documentation
Differentiate a matrix polynomial along the vector field U ↦ A U.
```
def matrixPolynomialDerivation {N : ℕ} :
    Matrix (Fin N) (Fin N) ℝ →ₗ[ℝ] Derivation ℝ (MatrixPolynomial N) (MatrixPolynomial N) where
…
```
Mentions: OAI.InvariantIsing.MatrixPolynomial
lemma OAI.InvariantIsing.matrixPolynomialDerivation_X line 29
lemma OAI.InvariantIsing.matrixPolynomialDerivation_mul_X line 34

theorem OAI.InvariantIsing.matrixPolynomialDerivation_commutator line 43

Source documentation

Left matrix vector fields give the opposite matrix Lie bracket.

theorem matrixPolynomialDerivation_commutator {N : ℕ}
    (A B : Matrix (Fin N) (Fin N) ℝ) :
    ⁅matrixPolynomialDerivation A,matrixPolynomialDerivation B⁆ =
      matrixPolynomialDerivation (B*A-A*B) := by
…

Mentions: OAI.InvariantIsing.matrixPolynomialDerivation

lemma OAI.InvariantIsing.matrixPolynomialDerivation_plane_X line 52