OAI/Probability/InvariantIsing/Cavity/CavityProjectorCoefficientError.lean
1 declarations, 0 contain sorry, 0 declared as axioms
A change of the small cavity blocks on a fixed spatial cutoff controls the normalized observable without inverse-normalizer estimates.
- theorem
OAI.InvariantIsing.cavity_projector_coefficient_errorline 17