OAI/Probability/InvariantIsing/Cavity/CavityCovariancePartitionBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The common root, all positive levels, and the residual have total covariance mass one. This estimate is independent of the number of steps.

  1. theorem OAI.InvariantIsing.cavity_covariance_partition_bound line 13
  2. theorem OAI.InvariantIsing.cavity_spectral_covariance_partition_bound line 56