OAI/Probability/InvariantIsing/Cavity/CavityGaussianPenaltyAlgebra.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite Gibbs algebra for absorbing a nonuniform covariance error by a penalty proportional to the squared cavity projection.

  1. lemma OAI.InvariantIsing.cavity_covariance_gibbs_bound line 14
  2. lemma OAI.InvariantIsing.cavity_covariance_penalty_nonneg line 62