OAI/Probability/InvariantIsing/Cavity/CavitySpectralCovariance.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A bound on the covariance in the actual quadratic Gibbs marginal. The innovation covariances are identified from their defining increments; their sum is controlled by the overlap partition, not by its number of cells.

  1. theorem OAI.InvariantIsing.cavity_spectral_total_covariance_bound line 16