OAI/Probability/InvariantIsing/Cavity/CavityHaarMarkedLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Weak convergence of the actual Haar cavity marks. In particular it applies to bounded replica tests with a hard spatial cutoff.

  1. theorem OAI.InvariantIsing.cavityHaarMarkedLaw_tendsto line 15
  2. theorem OAI.InvariantIsing.cavityGaussianMarkedLaw_radial_cutoff_tendsto line 51