OAI/Probability/InvariantIsing/Haar/MatrixRotation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Relating the orthogonal matrix and Euclidean-isometry models.

  1. lemma OAI.InvariantIsing.orthogonal_mulVec_norm_sq line 15

    Also declared: ComparatorChallenges/InvariantIsing.lean:41 (same declaration text).

  2. def OAI.InvariantIsing.matrixRotation line 29

    Source documentation

    An orthogonal matrix acts as a linear isometry in the pressure model.

    Also declared: ComparatorChallenges/InvariantIsing.lean:54 (same declaration text).

    def matrixRotation {N : ℕ} (U : Orthogonal N) : Rotation N :=
…

    Mentions: OAI.InvariantIsing.Orthogonal, OAI.InvariantIsing.Rotation

  3. lemma OAI.InvariantIsing.matrixRotation_apply line 36
  4. def OAI.InvariantIsing.specialRotation line 41

    Source documentation

    Restricting from O(N) to SO(N) preserves the same spectral action.

    def specialRotation {N : ℕ} (U : SpecialOrthogonal N) : Rotation N :=
…

    Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Rotation

  5. lemma OAI.InvariantIsing.specialRotation_apply line 44