OAI/Probability/InvariantIsing/Magnetic/RestrictedCanonicalLaw.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual canonical cutoff mean, with fixed tree, is exactly the restricted Haar Gibbs model used in the finite-replica comparison.

  1. theorem OAI.InvariantIsing.restricted_canonical_law line 17