OAI/Probability/InvariantIsing/Magnetic/RestrictedFieldFactorization.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The unrestricted recursion and its canonical transition are exactly products of the scalar field recursions.

  1. lemma OAI.InvariantIsing.fieldScalarValue_ofFn line 16
  2. theorem OAI.InvariantIsing.restrictedFieldRecursion_univ line 36
  3. lemma OAI.InvariantIsing.vectorGaussian_shift line 50
  4. lemma OAI.InvariantIsing.vectorGaussian_tilt_transition line 60