OAI/Probability/InvariantIsing/Cavity/CavityCappedSpinTest.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The paper's finite-spin cavity factor as a bounded continuous replica test, ready for the actual fresh-Haar / recalculated-cascade comparison.

  1. def OAI.InvariantIsing.cavityCappedSpinReplicaValue line 15
  2. lemma OAI.InvariantIsing.cavityCappedSpinReplicaValue_bound line 27
  3. lemma OAI.InvariantIsing.continuous_cavityCappedSpinReplicaValue line 48
  4. def OAI.InvariantIsing.cavityCappedSpinReplicaTest line 81