OAI/Probability/InvariantIsing/Cavity/CavityGibbsMeasureCovariance.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Equality of Gaussian field covariance identifies the law of the entire random Gibbs measure, so subsequent deterministic cavity reweighting and cutoff operations can use the same law.

  1. theorem OAI.InvariantIsing.cavity_gibbs_measure_same_covariance line 14