OAI/Probability/FreeIsing/Gibbs/CovarianceZero.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.HasFreeIsingLaw.finiteIsingPosterior_zero_eq_integral line 18
  2. theorem OAI.Problem367.finiteGibbsCovarianceOn_zero line 45
  3. theorem OAI.Problem367.finiteGibbsCovariance_zero line 59
  4. theorem OAI.Problem367.finiteGibbsPairMean_zero line 71
  5. theorem OAI.Problem367.infiniteGibbsPairMean_zero line 82
  6. theorem OAI.Problem367.infiniteGibbsCovariance_zero line 95
  7. theorem OAI.Problem367.infiniteGibbsResponse_zero line 102
  8. lemma OAI.Problem367.infiniteGibbsResponse_zero_sq line 109
  9. theorem OAI.Problem367.summable_infiniteGibbsResponse_zero_sq_iff line 115
  10. theorem OAI.Problem367.infiniteGibbsResponseRow_zero_of_strict line 134
  11. theorem OAI.Problem367.not_summable_infiniteGibbsResponse_zero_sq_of_critical line 146
  12. theorem OAI.Problem367.infiniteGibbsCovariance_brownian_zero line 154