OAI/Probability/PosteriorReplicas/Measures/EqualRightMeasure.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PosteriorReplicas.RightSource line 11
  2. def OAI.PosteriorReplicas.rightBaseSource line 13
  3. instance OAI.PosteriorReplicas.(instance at line 16) line 16
  4. def OAI.PosteriorReplicas.equalConstant line 21
  5. def OAI.PosteriorReplicas.rightBaseWeight line 23
  6. def OAI.PosteriorReplicas.residualRows line 26
  7. def OAI.PosteriorReplicas.rightBasePoint line 29
  8. lemma OAI.PosteriorReplicas.measurable_residualRows line 32
  9. lemma OAI.PosteriorReplicas.measurable_rightBasePoint line 37
  10. lemma OAI.PosteriorReplicas.measurable_rightBaseWeight line 40
  11. def OAI.PosteriorReplicas.rightBaseMeasure line 43
  12. lemma OAI.PosteriorReplicas.rightBaseWeight_integral_finite line 46
  13. lemma OAI.PosteriorReplicas.rightBaseMeasure_finite line 55
  14. lemma OAI.PosteriorReplicas.rightBaseMeasure_lintegral line 61
  15. lemma OAI.PosteriorReplicas.constrainedRows_eq_residualRows line 78
  16. lemma OAI.PosteriorReplicas.constrainedRows_eq_gaussianResidualRows line 84
  17. lemma OAI.PosteriorReplicas.rows_pairingsDensity_differences line 90
  18. lemma OAI.PosteriorReplicas.rightBaseMeasure_eq_equalLabelRight line 96
  19. lemma OAI.PosteriorReplicas.equalApprox_right_limit line 110