OAI/Probability/InvariantIsing/Cavity/CavitySpinFullLaw.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact full-factor spin law before and after the quadratic innovation change of variables. The ordinary residual is part of each probability.

  1. def OAI.InvariantIsing.cavityResidualSpinFullLaw line 14
  2. lemma OAI.InvariantIsing.cavityQuadraticResidualGibbs_eq_tilted line 24
  3. theorem OAI.InvariantIsing.cavityResidualSpinFullLaw_eq_successive line 40
  4. theorem OAI.InvariantIsing.cavity_full_spin_innovation_transport line 61