OAI/Probability/InvariantIsing/Fields/PriorFrozenGibbs.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Both selected perturbations reconstruct the same constrained Gibbs law.

  1. theorem OAI.InvariantIsing.priorFrozenGaussian_reference_fold_ae line 10
  2. theorem OAI.InvariantIsing.priorFrozenDiagonal_reference_fold_ae line 43