OAI/Probability/InvariantIsing/Spectral/SpectralPermutation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Spectral reorderings can be realized inside SO(N). A single row sign corrects a permutation determinant without changing any squared projection.

  1. lemma OAI.InvariantIsing.permutationMatrix_orthogonal line 15
  2. lemma OAI.InvariantIsing.permutationMatrix_det_sq line 21
  3. def OAI.InvariantIsing.permutationSignDiagonal line 27
  4. lemma OAI.InvariantIsing.permutationSignDiagonal_sq line 31
  5. lemma OAI.InvariantIsing.permutationSignDiagonal_det line 43
  6. def OAI.InvariantIsing.spectralPermutation line 48

    Source documentation

    A permutation of spectral coordinates, with determinant corrected to one.

    def spectralPermutation {N : ℕ} (hN : 0 < N) (p : Equiv.Perm (Fin N)) :
    SpecialOrthogonal N :=
…

    Mentions: OAI.InvariantIsing.SpecialOrthogonal

  7. lemma OAI.InvariantIsing.spectralPermutation_coordinate_sq line 65
  8. lemma OAI.InvariantIsing.rotatedEnergy_spectralPermutation line 84
  9. lemma OAI.InvariantIsing.meanPressure_spectralPermutation line 91