OAI/Probability/InvariantIsing/Cavity/CavityCutoffRadii.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

One sequence of increasing cutoff radii can avoid every boundary atom of a countable family of limiting replica laws.

  1. lemma OAI.InvariantIsing.cavity_radius_atoms_countable line 15
  2. theorem OAI.InvariantIsing.cavity_common_null_cutoff_radii line 24