OAI/Probability/InvariantIsing/Gaussian/GordonCovariance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Covariance contraction of the two-level Gaussian integration-by-parts identity.

  1. lemma OAI.InvariantIsing.gordonRowMean_linear_sum line 13
  2. lemma OAI.InvariantIsing.gordonMean_linear_sum line 26
  3. lemma OAI.InvariantIsing.gordon_covariance_contraction line 39
  4. theorem OAI.InvariantIsing.gordon_gaussian_covariance_insertion line 60