OAI/Probability/InvariantIsing/Cavity/CavityGaussianRoot.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The ordinary, exponent-zero Gaussian expectation at the common root of the quadratic cavity recursion.

  1. lemma OAI.InvariantIsing.cavity_gaussian_eval_memLp line 14
  2. lemma OAI.InvariantIsing.cavity_gaussian_eval_integral line 20
  3. lemma OAI.InvariantIsing.cavity_gaussian_eval_mul_integral line 26
  4. lemma OAI.InvariantIsing.cavity_quadratic_as_sum line 34
  5. theorem OAI.InvariantIsing.cavity_gaussian_root_integrable line 46
  6. theorem OAI.InvariantIsing.cavity_gaussian_root_integral line 58