OAI/Probability/InvariantIsing/Cavity/CavityCanonicalRestrictedLaw.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.cavity_canonical_restricted_law line 16