OAI/Probability/InvariantIsing/Magnetic/RestrictedGeometricWeightedTest.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual original-model cutoff comparison in base Gibbs variables, with its weight identified as the physical finite-block cavity factor.

  1. theorem OAI.InvariantIsing.restricted_geometric_weighted_test line 16