OAI/Probability/GaussianReplacement/Posterior.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentProjection.criticalSignal line 13
2. instance OAI.CurrentProjection.criticalSignal_probability line 17
3. def OAI.CurrentProjection.criticalB line 23
4. def OAI.CurrentProjection.criticalD line 27
5. lemma OAI.CurrentProjection.criticalSignal_fst line 31
6. lemma OAI.CurrentProjection.criticalSignal_posterior line 37
7. lemma OAI.CurrentProjection.criticalB_eq line 62
8. lemma OAI.CurrentProjection.criticalD_eq line 82
9. lemma OAI.CurrentProjection.criticalFamily_growth line 89
10. lemma OAI.CurrentProjection.criticalSignal_entropy line 130
11. lemma OAI.CurrentProjection.criticalLevel_integrable line 144
12. lemma OAI.CurrentProjection.criticalFamily_moment_mean line 173
13. lemma OAI.CurrentProjection.completeFamily_restrict_apply line 222
14. lemma OAI.CurrentProjection.completeFamily_restrict_ae line 228
15. lemma OAI.CurrentProjection.actual_posterior_completed line 234
16. lemma OAI.CurrentProjection.actualRowConclusion_observed line 280
17. lemma OAI.CurrentProjection.observedMessage_aligned_positive line 320
18. lemma OAI.CurrentProjection.actual_posterior_log_bound line 332
19. lemma OAI.CurrentProjection.criticalFamily_cover_fibre line 379
20. lemma OAI.CurrentProjection.criticalFamily_cover_mean line 408
21. def OAI.CurrentProjection.refineRows line 469
22. lemma OAI.CurrentProjection.measurable_refineRowsMap line 474
23. lemma OAI.CurrentProjection.refineRows_probability line 479
24. lemma OAI.CurrentProjection.refineRows_fst line 486
25. lemma OAI.CurrentProjection.refineRows_signal_rows line 494
26. lemma OAI.CurrentProjection.refineRows_drop line 502
27. lemma OAI.CurrentProjection.alignedExperiment_drop line 510
28. lemma OAI.CurrentProjection.independent_refineSignal_drop line 526
29. lemma OAI.CurrentProjection.alignedExperiment_independent line 540
30. lemma OAI.CurrentProjection.signal_marginal_of_independence line 551