OAI/Probability/InvariantIsing/Magnetic/RestrictedFieldRecursion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual vector Gaussian recursion for a constrained cavity block. Regularity follows from the terminal's finite-spin estimates, with no assumption on the number of cascade levels.

  1. def OAI.InvariantIsing.restrictedFieldRecursion line 17
  2. lemma OAI.InvariantIsing.restrictedFieldRecursion_regular line 22
  3. lemma OAI.InvariantIsing.restrictedFieldRecursion_lipschitz line 32
  4. lemma OAI.InvariantIsing.integrable_exp_restrictedFieldRecursion line 41
  5. lemma OAI.InvariantIsing.restrictedFieldRecursion_root_integrable line 50
  6. def OAI.InvariantIsing.constrainedBlockValue line 68
  7. lemma OAI.InvariantIsing.constrainedBlockValue_root_integrable line 74