OAI/Probability/InvariantIsing/Cavity/CavityNormalizedCoefficientLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual normalized projector-cavity tests tolerate random coefficient replacement in probability. No moment or inverse-partition assumption is added on a fixed spatial cutoff.

  1. theorem OAI.InvariantIsing.cavity_normalized_coefficient_tendsto line 16