OAI/Probability/InvariantIsing/Haar/HaarCasimirAlgebra.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Adjoint invariance of the quadratic orthogonal Casimir in any representation.

  1. lemma OAI.InvariantIsing.sum_skew_symmetric_coeff_swap line 11
  2. theorem OAI.InvariantIsing.plane_adjoint_jordan_sum line 20

    Source documentation

    The coefficient cancellation uses only skew symmetry, with no analytic premise.

    theorem plane_adjoint_jordan_sum {N : ℕ} {V : Type*}
    [AddCommGroup V] [Module ℝ V]
    (F : Matrix (Fin N) (Fin N) ℝ →ₗ[ℝ] Module.End ℝ V)
    (A : Matrix (Fin N) (Fin N) ℝ) (hA : A.transpose = -A) :
    (∑ i, ∑ j,
      (F (planeGenerator i j)*F (A*planeGenerator i j-planeGenerator i j*A)+
       F (A*planeGenerator i j-planeGenerator i j*A)*F (planeGenerator i j))) = 0 := by
…

    Mentions: OAI.InvariantIsing.planeGenerator