OAI/Probability/InvariantIsing/Cavity/CavityGroupGibbsAverage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Fresh independent rotations inside the spectral groups can be inserted in every bounded replica observable of the actual perturbed Gibbs law. Its diagonal and tensor perturbations are both retained.

  1. lemma OAI.InvariantIsing.measurable_cavityRotationReplicaMean line 16
  2. theorem OAI.InvariantIsing.cavity_group_gibbs_average line 29