OAI/Probability/InvariantIsing/Cavity/CavityGeometricTail.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The full-model cutoff estimate for the actual normalized spectral image construction, with no inverse-Gram estimate on the bad event.

  1. lemma OAI.InvariantIsing.measurable_cavityFullSpecialCoordinates line 15
  2. theorem OAI.InvariantIsing.cavity_full_geometric_tail line 44