OAI/Probability/PosteriorReplicas/Gaussian/GaussianFiber.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PosteriorReplicas.charFun_gaussian_starProjection line 16
  2. lemma OAI.PosteriorReplicas.gaussian_orthogonal_sum line 25
  3. lemma OAI.PosteriorReplicas.gaussian_orthogonal_pair line 47
  4. lemma OAI.PosteriorReplicas.gaussian_orthogonal_indep line 76
  5. lemma OAI.PosteriorReplicas.pairing_starProjection line 83
  6. lemma OAI.PosteriorReplicas.orthonormal_starProjection line 88
  7. lemma OAI.PosteriorReplicas.gaussian_pairings_residual_indep line 104
  8. lemma OAI.PosteriorReplicas.gaussian_orthonormal_pair line 116
  9. lemma OAI.PosteriorReplicas.gaussian_orthonormal_disintegration line 124
  10. def OAI.PosteriorReplicas.pairingLift line 138
  11. lemma OAI.PosteriorReplicas.pairingLift_mem line 142
  12. lemma OAI.PosteriorReplicas.pairings_pairingLift line 150
  13. lemma OAI.PosteriorReplicas.starProjection_eq_pairingLift line 161
  14. lemma OAI.PosteriorReplicas.continuous_pairingLift line 178
  15. lemma OAI.PosteriorReplicas.gaussian_pairings_disintegration line 182
  16. lemma OAI.PosteriorReplicas.gaussian_pairings_integral line 199