OAI/Probability/InvariantIsing/Haar/HaarPlaneFrame.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact coordinate-plane frame identities in the skew matrix space.

  1. lemma OAI.InvariantIsing.planeGenerator_swap line 11
  2. lemma OAI.InvariantIsing.sum_entry_planeGenerator line 15
  3. lemma OAI.InvariantIsing.matrixFrobeniusPair_eq_sum line 23
  4. lemma OAI.InvariantIsing.matrixFrobeniusPair_plane line 29
  5. lemma OAI.InvariantIsing.skew_matrix_bracket line 36
  6. lemma OAI.InvariantIsing.matrixFrobeniusPair_plane_skew line 41
  7. lemma OAI.InvariantIsing.sum_matrixFrobeniusPair_plane_sq line 48
  8. lemma OAI.InvariantIsing.plane_functional_representation line 57

    Source documentation

    A linear functional on skew matrices is represented by its plane coordinates.

    lemma plane_functional_representation {N : ℕ}
    (ell : Matrix (Fin N) (Fin N) ℝ →ₗ[ℝ] ℝ)
    (B : Matrix (Fin N) (Fin N) ℝ) (hB : B.transpose = -B) :
    matrixFrobeniusPair (Matrix.of fun i j => ell (planeGenerator i j)) B = 2*ell B := by
…

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