OAI/Probability/InvariantIsing/Haar/HaarPolynomialLaplacian.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The polynomial Laplacian on the orthogonal group commutes with rotations.

  1. def OAI.InvariantIsing.matrixPolynomialOperator line 12
  2. lemma OAI.InvariantIsing.matrixPolynomialOperator_apply line 18
  3. lemma OAI.InvariantIsing.matrixPolynomialOperator_commutator line 22
  4. lemma OAI.InvariantIsing.commutator_square_identity line 31
  5. def OAI.InvariantIsing.haarPolynomialLaplacian line 36

    Source documentation

    Ordered coordinate planes; its carré du champ is the sum of the ordered squares.

    def haarPolynomialLaplacian (N : ℕ) : Module.End ℝ (MatrixPolynomial N) :=
…

    Mentions: OAI.InvariantIsing.MatrixPolynomial

  6. theorem OAI.InvariantIsing.haarPolynomialLaplacian_commutes line 40
  7. lemma OAI.InvariantIsing.haarPolynomialLaplacian_apply line 61
  8. lemma OAI.InvariantIsing.haarPolynomialLaplacian_derivation line 68