OAI/Probability/InvariantIsing/Arrays/TensorFrozenGibbs.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.tensorFrozenGaussian_reference_fold_ae line 13
  2. theorem OAI.InvariantIsing.tensorFrozenDiagonal_reference_fold_ae line 52