OAI/Probability/FreeIsing/Gibbs/CovarianceEnergy.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.finiteGibbsCovarianceOn_eq_treeCovariance line 16
  2. theorem OAI.Problem367.TreePathResponse.covariance_sq_le_response_sq line 24
  3. theorem OAI.Problem367.finiteGibbsCovariance_sq_le_observedRow_sq line 36
  4. lemma OAI.Problem367.integrable_finiteGibbsCovariance_sq line 49
  5. lemma OAI.Problem367.integrable_infiniteGibbsCovariance_sq line 63
  6. theorem OAI.Problem367.integral_finiteGibbsCovariance_sq_le line 77
  7. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsCovariance_tendsto_integral_sq line 92
  8. theorem OAI.Problem367.HasFreeIsingLaw.integral_infiniteGibbsCovariance_sq_le line 114
  9. theorem OAI.Problem367.HasFreeIsingLaw.ae_summable_infiniteGibbsCovariance_sq line 125
  10. theorem OAI.Problem367.HasFreeIsingLaw.integral_infiniteGibbsCovariance_energy_le line 141
  11. theorem OAI.Problem367.HasFreeIsingLaw.integral_infiniteGibbsCovariance_energy_tail_le line 159
  12. lemma OAI.Problem367.integrable_finiteGibbsCovariance_sub_infinite_sq line 179
  13. theorem OAI.Problem367.HasFreeIsingLaw.integral_finiteGibbsCovariance_sub_infinite_sq_le line 193
  14. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsCovariance_tendsto_rowMeanSquare line 229
  15. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsCovariance_tendsto_integral_rowMeanSquare line 249