OAI/Probability/InvariantIsing/Magnetic/RestrictedProjectorCoefficientError.lean

GitHub source file

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.

  1. theorem OAI.InvariantIsing.restricted_projector_coefficient_error line 17