OAI/Probability/PosteriorReplicas/Gaussian/GaussianDensity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PosteriorReplicas.matrixLinearEquiv line 11
  2. lemma OAI.PosteriorReplicas.gaussian_linear_image_density line 26
  3. lemma OAI.PosteriorReplicas.gaussian_density_product line 39
  4. def OAI.PosteriorReplicas.pairingTriangular line 60
  5. lemma OAI.PosteriorReplicas.pairingTriangular_expansion line 63
  6. lemma OAI.PosteriorReplicas.pairingTriangular_det line 75
  7. lemma OAI.PosteriorReplicas.pairingTriangular_det_pos line 83
  8. lemma OAI.PosteriorReplicas.pairings_eq_triangular line 88
  9. lemma OAI.PosteriorReplicas.gaussian_pairings_density_coordinates line 96
  10. lemma OAI.PosteriorReplicas.orthonormal_pairings_eq_inverse line 107
  11. lemma OAI.PosteriorReplicas.pairingLift_energy line 118
  12. lemma OAI.PosteriorReplicas.gaussian_pairings_density line 134
  13. lemma OAI.PosteriorReplicas.gaussian_fiber_integral line 147