OAI/Probability/InvariantIsing/Cavity/CavityGroupGibbsInvariant.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual Gaussian perturbation respects rotations inside every base spectral group, after averaging over the Gaussian disorder.

  1. lemma OAI.InvariantIsing.cavityGroup_diagonal_eigenvalues line 17
  2. theorem OAI.InvariantIsing.cavityGroupRotation_perturbed_energy line 26
  3. theorem OAI.InvariantIsing.cavityGroupRotation_perturbation_covariance line 38
  4. theorem OAI.InvariantIsing.cavityGroupRotation_gibbs_replica line 53