OAI/Probability/InvariantIsing/Cavity/CavityStrictMarkedLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The strict finite Gaussian cavity laws and the physical Haar marks have the same weak limit. The identification uses the proved spectral GG and Ward consequences through the finite cascade comparison.

  1. theorem OAI.InvariantIsing.cavity_strict_marked_law_tendsto line 16