OAI/Probability/PosteriorReplicas/Geometry/TupleMoments.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorReplicas.continuous_differences line 11
2. lemma OAI.PosteriorReplicas.continuous_affineVolume line 15
3. lemma OAI.PosteriorReplicas.measurableSet_row_independent line 22
4. lemma OAI.PosteriorReplicas.measurableSet_affine_independent line 31
5. lemma OAI.PosteriorReplicas.differences_cons line 35
6. lemma OAI.PosteriorReplicas.ae_base_tuple_full_rank line 40
7. lemma OAI.PosteriorReplicas.ae_gaussian_rows_full_rank line 51
8. lemma OAI.PosteriorReplicas.base_tuple_inverse_finite line 57
9. lemma OAI.PosteriorReplicas.gaussian_rows_inverse_finite line 85
10. lemma OAI.PosteriorReplicas.base_density_sup_moment_finite line 91