OAI/Probability/InvariantIsing/Cavity/CavityDisorderTestComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Averaging the actual full/base cutoff comparison over the coupled spectral geometry. No uniformity in the unbounded interaction energy is needed: the explicit error depends only on the geometric cutoff.

  1. def OAI.InvariantIsing.cavityBaseCutoffReplicaMean line 16
  2. def OAI.InvariantIsing.cavityFullCutoffReplicaMean line 28
  3. theorem OAI.InvariantIsing.cavity_disorder_cutoff_test_comparison line 38