OAI/Probability/PosteriorReplicas/Kernels/KernelPi.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.PosteriorReplicas.measurable_fin_consline 10 - def
OAI.PosteriorReplicas.piKernelline 18 - instance
OAI.PosteriorReplicas.piKernel_markovline 24 - lemma
OAI.PosteriorReplicas.piKernel_applyline 34 - lemma
OAI.PosteriorReplicas.measurable_piKernelline 51