OAI/Probability/InvariantIsing/Cavity/CavityCutoffFloorLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The order of the two remaining limits: choose a large spatial radius, then a small denominator floor, then pass to the system-size limit.

  1. theorem OAI.InvariantIsing.cavity_cutoff_floor_comparison line 14
  2. theorem OAI.InvariantIsing.cavity_limit_of_eventual_cutoff_comparison line 43