OAI/Probability/PosteriorReplicas/Information/ObservableLikelihood.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PosteriorReplicas.AuxSpace line 12
  2. def OAI.PosteriorReplicas.auxLaw line 14
  3. instance OAI.PosteriorReplicas.(instance at line 17) line 17
  4. def OAI.PosteriorReplicas.projectedTuple line 20
  5. lemma OAI.PosteriorReplicas.measurable_projectedTuple line 23
  6. lemma OAI.PosteriorReplicas.differences_projectedTuple line 27
  7. def OAI.PosteriorReplicas.observableRows line 32
  8. lemma OAI.PosteriorReplicas.measurable_observableRows line 35
  9. lemma OAI.PosteriorReplicas.observableRows_law line 39
  10. abbrev OAI.PosteriorReplicas.Observation line 53
  11. def OAI.PosteriorReplicas.observe line 55
  12. lemma OAI.PosteriorReplicas.measurable_observe line 58
  13. def OAI.PosteriorReplicas.observableLikelihood line 61
  14. lemma OAI.PosteriorReplicas.measurable_observableLikelihood line 69
  15. lemma OAI.PosteriorReplicas.observableLikelihood_observe line 73
  16. lemma OAI.PosteriorReplicas.observableLikelihood_fixed_lintegral line 95
  17. lemma OAI.PosteriorReplicas.equalReference_tuple line 132
  18. lemma OAI.PosteriorReplicas.observableLikelihood_lintegral line 138
  19. lemma OAI.PosteriorReplicas.observableDensity_expected line 175