OAI/Probability/InvariantIsing/Cavity/CavityGaussianAffine.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Affine quadratic Gaussian integrals. Independent linear terms are needed after diagonalizing the precision of a noncommuting cavity tilt.

  1. lemma OAI.InvariantIsing.cavity_affine_complete_square line 14
  2. lemma OAI.InvariantIsing.cavity_affine_constant line 22
  3. lemma OAI.InvariantIsing.cavity_gaussian_linear_integral line 30
  4. theorem OAI.InvariantIsing.cavity_gaussian_affine_integrable line 36
  5. theorem OAI.InvariantIsing.cavity_gaussian_affine_integral line 46
  6. theorem OAI.InvariantIsing.cavity_gaussian_affine_logIntegral line 60
  7. theorem OAI.InvariantIsing.cavity_diagonal_gaussian_affine_integrable line 69
  8. theorem OAI.InvariantIsing.cavity_diagonal_gaussian_affine_integral line 80