OAI/Probability/InvariantIsing/Cavity/CavityBaseCutoffFactor.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Factoring a restricted cavity test over the base Gibbs law. The cutoff remains inside the weight, so its zero convention is preserved.

  1. lemma OAI.InvariantIsing.cavity_reference_tilt_add line 15
  2. lemma OAI.InvariantIsing.cavity_cutoff_tilt_add line 31
  3. theorem OAI.InvariantIsing.cavity_base_cutoff_indicator line 43