OAI/Probability/InvariantIsing/Cavity/CavityGeometricTest.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual retained-projector coupling supplies the geometric error needed for every bounded replica test on a fixed special-coordinate cutoff.

  1. def OAI.InvariantIsing.cavityGeometricWeight line 15
  2. lemma OAI.InvariantIsing.cavityGeometricWeight_one_le line 20
  3. theorem OAI.InvariantIsing.cavity_geometric_cutoff_test line 25