OAI/Probability/InvariantIsing/Cavity/CavityCascadeMarkedLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Joint Gaussian marks and every synchronized finite overlap label pass to the rounded-cascade limit, including singular covariances.

  1. theorem OAI.InvariantIsing.cavity_cascade_marked_block_tendsto line 15