OAI/Probability/InvariantIsing/Fields/SpinPriorFrozenGibbs.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Frozen Gaussian and diagonal tilts reconstruct the same actual Gibbs law.

  1. theorem OAI.InvariantIsing.spinPriorFrozenGaussian_reference_fold_ae line 13
  2. theorem OAI.InvariantIsing.spinPriorFrozenDiagonal_reference_fold_ae line 55