OAI/Probability/FreeIsing/Gaussian/TreeCovariance.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.GaussianTreeCovariance.covariance line 13
  2. lemma OAI.Problem367.GaussianTreeCovariance.measurable_covariance line 20
  3. lemma OAI.Problem367.GaussianTreeCovariance.covariance_congr line 26
  4. lemma OAI.Problem367.GaussianTreeCovariance.covariance_bounds line 38
  5. lemma OAI.Problem367.GaussianTreeCovariance.covariance_erase line 47
  6. lemma OAI.Problem367.GaussianTreeCovariance.covariance_leaf line 58
  7. lemma OAI.Problem367.GaussianTreeCovariance.measurable_covariance_sq line 75
  8. lemma OAI.Problem367.GaussianTreeCovariance.covariance_updated_fields line 82
  9. lemma OAI.Problem367.GaussianTreeCovariance.lmarginal_leaf line 104
  10. lemma OAI.Problem367.GaussianTreeCovariance.lmarginal_nonleaf line 126
  11. theorem OAI.Problem367.GaussianTreeCovariance.lmarginal_covariance_sq_le line 144
  12. def OAI.Problem367.GaussianTreeCovariance.gaussianContraction line 241
  13. lemma OAI.Problem367.GaussianTreeCovariance.gaussianContraction_pos line 244
  14. lemma OAI.Problem367.GaussianTreeCovariance.gaussianContraction_lt_one line 252
  15. lemma OAI.Problem367.GaussianTreeCovariance.lintegral_gaussian_attenuation_le line 262
  16. theorem OAI.Problem367.GaussianTreeCovariance.lintegral_gaussian_covariance_sq_le line 283
  17. lemma OAI.Problem367.GaussianTreeCovariance.integrable_covariance_sq line 303
  18. theorem OAI.Problem367.GaussianTreeCovariance.integral_gaussian_covariance_sq_le line 326