OAI/Probability/InvariantIsing/Cavity/CavityResidualSpinSampling.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integrating the ordinary Gaussian residual in the actual joint Gibbs law leaves the finite Ising Gibbs law of the effective scalar field.

  1. lemma OAI.InvariantIsing.cavity_residual_spin_weight_integrable line 15
  2. theorem OAI.InvariantIsing.cavity_residual_spin_weight_integral line 29
  3. theorem OAI.InvariantIsing.cavity_residual_spin_gibbs_test line 42
  4. theorem OAI.InvariantIsing.cavity_residual_spin_coordinate_mean line 59