OAI/Probability/PosteriorReplicas/Gaussian/GaussianRowMix.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PosteriorReplicas.matrixNormal_density line 11
  2. lemma OAI.PosteriorReplicas.matrixNormal_transpose line 23
  3. lemma OAI.PosteriorReplicas.gaussianRows_eq_matrixNormal line 35
  4. def OAI.PosteriorReplicas.vecTranspose line 41
  5. lemma OAI.PosteriorReplicas.measurable_vecTranspose line 44
  6. lemma OAI.PosteriorReplicas.vecTranspose_involutive line 48
  7. lemma OAI.PosteriorReplicas.gaussianRows_transpose line 51
  8. def OAI.PosteriorReplicas.rowMix line 57
  9. lemma OAI.PosteriorReplicas.measurable_rowMix line 60
  10. lemma OAI.PosteriorReplicas.rowMix_apply line 65
  11. lemma OAI.PosteriorReplicas.gaussianRows_mix line 69
  12. lemma OAI.PosteriorReplicas.rowMix_starProjection line 90
  13. lemma OAI.PosteriorReplicas.gaussianRows_mix_projected line 96