OAI/Probability/PosteriorReplicas/Measures/EqualBaseMeasures.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PosteriorReplicas.EqualSpace line 11
  2. abbrev OAI.PosteriorReplicas.LeftSource line 12
  3. def OAI.PosteriorReplicas.leftBaseSource line 14
  4. instance OAI.PosteriorReplicas.(instance at line 17) line 17
  5. def OAI.PosteriorReplicas.leftBasePoint line 22
  6. def OAI.PosteriorReplicas.leftBaseWeight line 26
  7. lemma OAI.PosteriorReplicas.measurable_leftBasePoint line 29
  8. lemma OAI.PosteriorReplicas.measurable_leftBaseWeight line 34
  9. def OAI.PosteriorReplicas.leftBaseMeasure line 39
  10. lemma OAI.PosteriorReplicas.leftBaseWeight_integral_finite line 42
  11. lemma OAI.PosteriorReplicas.leftBaseMeasure_finite line 54
  12. lemma OAI.PosteriorReplicas.leftBaseMeasure_lintegral line 60
  13. lemma OAI.PosteriorReplicas.leftBaseMeasure_lintegral_fibers line 81
  14. lemma OAI.PosteriorReplicas.tiltMass_one line 105
  15. lemma OAI.PosteriorReplicas.tiltedFiber_one line 108
  16. lemma OAI.PosteriorReplicas.leftBaseMeasure_eq_equalLabelLeft line 112