OAI/Probability/PosteriorReplicas/Information/StateExperiment.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PosteriorReplicas.initialStateKernel line 11
2. instance OAI.PosteriorReplicas.(instance at line 14) line 14
3. lemma OAI.PosteriorReplicas.initialStateKernel_marginal line 17
4. lemma OAI.PosteriorReplicas.lintegral_initialStateKernel line 23
5. def OAI.PosteriorReplicas.stateBlockKernel line 34
6. instance OAI.PosteriorReplicas.(instance at line 37) line 37
7. def OAI.PosteriorReplicas.stateOutputKernel line 40
8. instance OAI.PosteriorReplicas.(instance at line 44) line 44
9. lemma OAI.PosteriorReplicas.stateOutputKernel_apply line 50
10. lemma OAI.PosteriorReplicas.signalMessageLaw_lintegral line 54
11. lemma OAI.PosteriorReplicas.stateMessageLaw_lintegral line 65
12. lemma OAI.PosteriorReplicas.stateMessageLaw_eq_compProd line 76
13. lemma OAI.PosteriorReplicas.stateMessageLaw_state_terminal line 90
14. lemma OAI.PosteriorReplicas.stateMessageLaw_initial line 97
15. lemma OAI.PosteriorReplicas.terminalConditionalEntropy_average line 104