OAI/Probability/InvariantIsing/Fields/FieldSpinProduct.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The finite Ising spin law with a scalar field at each site factors into the actual one-site Gibbs kernels, including its two-spin tests.

  1. lemma OAI.InvariantIsing.uniformSpinPrior_eq_product line 15
  2. theorem OAI.InvariantIsing.fieldSpinGibbs_eq_product line 26
  3. theorem OAI.InvariantIsing.fieldSpinGibbs_coordinate_mean line 51
  4. theorem OAI.InvariantIsing.fieldSpinGibbs_pair_mean line 59