OAI/Probability/InvariantIsing/Cavity/CavityResidualSpinLaw.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The residual-integrated Gibbs spin marginal, as an equality of probability measures, and its independent two-replica consequence.

  1. theorem OAI.InvariantIsing.cavity_residual_spin_gibbs_map line 14
  2. theorem OAI.InvariantIsing.cavity_residual_spin_pair_mean line 35