OAI/Probability/PosteriorReplicas/Gaussian/MatrixNoise.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PosteriorReplicas.transposeCLE line 10
  2. lemma OAI.PosteriorReplicas.transposeCLE_apply line 19
  3. lemma OAI.PosteriorReplicas.matrix_volume_unit_cube line 22
  4. instance OAI.PosteriorReplicas.matrixPiVolumeAddHaar line 28
  5. lemma OAI.PosteriorReplicas.transpose_volume_preserving line 32
  6. def OAI.PosteriorReplicas.matrixNormal line 52
  7. instance OAI.PosteriorReplicas.(instance at line 55) line 55
  8. def OAI.PosteriorReplicas.noiseScale line 59
  9. lemma OAI.PosteriorReplicas.noiseScale_pos line 61
  10. lemma OAI.PosteriorReplicas.tendsto_noiseScale line 62
  11. def OAI.PosteriorReplicas.matrixNoiseDensity line 65
  12. lemma OAI.PosteriorReplicas.measurable_matrixNoiseDensity line 68
  13. lemma OAI.PosteriorReplicas.matrixNormal_scale line 73
  14. lemma OAI.PosteriorReplicas.matrix_noise_shrinks line 106
  15. lemma OAI.PosteriorReplicas.matrixNoise_convolution line 113
  16. lemma OAI.PosteriorReplicas.matrixNoise_transpose_lintegral line 127