OAI/Probability/InvariantIsing/Cavity/CavityGaussianRotation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Orthogonal invariance of the finite Gaussian array, expressed as a simultaneous rotation of all its columns.

  1. def OAI.InvariantIsing.cavityColumnEquiv line 17
  2. lemma OAI.InvariantIsing.cavityColumnEquiv_apply line 24
  3. lemma OAI.InvariantIsing.cavityColumnEquiv_symm_apply line 28
  4. def OAI.InvariantIsing.cavityColumnRotation line 32
  5. lemma OAI.InvariantIsing.cavityColumnRotation_apply line 38
  6. theorem OAI.InvariantIsing.cavityColumnRotation_gaussian line 44
  7. def OAI.InvariantIsing.cavityArrayMatrix line 50
  8. lemma OAI.InvariantIsing.cavityArrayMatrix_rotation line 53
  9. lemma OAI.InvariantIsing.cavityArrayFrame_rotation line 61
  10. def OAI.InvariantIsing.cavityFrameLaw line 69
  11. theorem OAI.InvariantIsing.cavityFrameLaw_rotation line 75

    Source documentation

    The finite Gaussian construction is exactly invariant under rotations of the ambient space, before passing to the large-dimension limit.

    theorem cavityFrameLaw_rotation {n q : ℕ} (U : Orthogonal n) :
    (cavityFrameLaw n q).map (fun A => (U : Matrix (Fin n) (Fin n) ℝ) * A) =
      cavityFrameLaw n q := by
…

    Mentions: OAI.InvariantIsing.Orthogonal, OAI.InvariantIsing.cavityFrameLaw