OAI/Probability/FreeIsing/Posterior/ArrayPosteriorCovarianceStationarity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem367.ArrayPosteriorStationarity.integrable_spin_pair line 14
2. def OAI.Problem367.ArrayPosteriorStationarity.posteriorPair line 26
3. def OAI.Problem367.ArrayPosteriorStationarity.posteriorCovariance line 33
4. lemma OAI.Problem367.ArrayPosteriorStationarity.measurable_posteriorPair line 40
5. lemma OAI.Problem367.ArrayPosteriorStationarity.measurable_posteriorCovariance line 46
6. theorem OAI.Problem367.ArrayPosteriorStationarity.posteriorPair_relabel_ae line 53
7. theorem OAI.Problem367.ArrayPosteriorStationarity.posteriorCovariance_relabel_ae line 69
8. theorem OAI.Problem367.ArrayPosteriorStationarity.posteriorCovariance_version_relabel_ae line 83
9. theorem OAI.Problem367.ArrayPosteriorStationarity.posteriorCovariance_version_matrix_relabel_ae line 98