OAI/Probability/InvariantIsing/Haar/HaarFrobeniusBracket.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The exact Frobenius bracket contraction for the special orthogonal algebra.

  1. def OAI.InvariantIsing.matrixFrobeniusPair line 12

    Source documentation

    The real, unnormalized Frobenius bilinear form.

    def matrixFrobeniusPair {N : ℕ} (A B : Matrix (Fin N) (Fin N) ℝ) : ℝ :=
…
  2. lemma OAI.InvariantIsing.matrixFrobeniusPair_self line 15
  3. lemma OAI.InvariantIsing.matrixFrobeniusPair_self_nonneg line 21
  4. lemma OAI.InvariantIsing.planeGenerator_transpose line 26
  5. lemma OAI.InvariantIsing.matrixFrobeniusPair_bracket line 30
  6. theorem OAI.InvariantIsing.sum_planeGenerator_bracket_norm_sq line 42

    Source documentation

    Ordered coordinate planes count each orthogonal tangent direction twice.

    theorem sum_planeGenerator_bracket_norm_sq {N : ℕ}
    (A : Matrix (Fin N) (Fin N) ℝ) (hA : A.transpose = -A) :
    (∑ i : Fin N, ∑ j : Fin N,
      matrixFrobeniusPair (planeGenerator i j*A-A*planeGenerator i j)
        (planeGenerator i j*A-A*planeGenerator i j)) =
      (4*((N : ℝ)-2))*matrixFrobeniusPair A A := by
…

    Mentions: OAI.InvariantIsing.matrixFrobeniusPair, OAI.InvariantIsing.planeGenerator