OAI/Probability/InvariantIsing/Cavity/CavityDisorderLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual finite perturbation comparison vanishes on every fixed geometric cutoff, also after averaging over a varying disorder space.

  1. lemma OAI.InvariantIsing.cavityCylinderReplicaMean_abs_le line 14
  2. theorem OAI.InvariantIsing.cavity_disorder_cutoff_difference_tendsto line 27