OAI/Probability/PosteriorReplicas/Gaussian/GramTransform.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PosteriorReplicas.columnMix line 13
2. lemma OAI.PosteriorReplicas.measurable_columnMix line 16
3. lemma OAI.PosteriorReplicas.gram_columnMix line 22
4. lemma OAI.PosteriorReplicas.gramVolume_columnMix line 27
5. lemma OAI.PosteriorReplicas.columnMix_independent line 34
6. def OAI.PosteriorReplicas.pairingColumns line 41
7. lemma OAI.PosteriorReplicas.measurable_pairingColumns line 44
8. lemma OAI.PosteriorReplicas.pairingColumns_triangular line 49
9. lemma OAI.PosteriorReplicas.orthonormal_pairingColumns_law line 57
10. lemma OAI.PosteriorReplicas.pairingColumns_law line 66
11. lemma OAI.PosteriorReplicas.ae_pairingColumns_independent line 74
12. lemma OAI.PosteriorReplicas.gramVolume_pairingColumns line 86