OAI/Probability/FreeIsing/Gibbs/CovarianceL2Limit.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.finiteGibbsCovarianceOn line 17
  2. lemma OAI.Problem367.continuous_finiteGibbsCovarianceOn line 29
  3. lemma OAI.Problem367.finiteGibbsCovarianceOn_abs_le_two line 36
  4. def OAI.Problem367.finiteGibbsCovariance line 62
  5. lemma OAI.Problem367.continuous_finiteGibbsCovariance line 70
  6. lemma OAI.Problem367.finiteGibbsCovariance_abs_le_two line 79
  7. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsCovarianceOn_eq_posterior line 88
  8. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsCovariance_tendsto_ae line 106
  9. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsCovariance_tendsto_meanSquare line 144
  10. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsCovariance_brownian_tendsto_ae line 161
  11. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsCovariance_brownian_tendsto_meanSquare line 184
  12. lemma OAI.Problem367.measurable_brownian_ising_observation_uncurry line 215
  13. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsCovariance_brownian_tendsto_timeMeanSquare line 234