OAI/Probability/InvariantIsing/Cavity/CavityHaarRestrictedRegularized.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual physical Haar Gibbs means and the finite cascade agree after spatial restriction and fixed positive denominator regularization.

  1. theorem OAI.InvariantIsing.cavity_haar_restricted_gibbs_regularized_match line 16