OAI/Probability/SKGap/Posterior/StaticExperimentBridge.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.FullMain.halfDiff_sq line 19
2. lemma OAI.SKGap.FullMain.conditionalVariance_eq line 25
3. lemma OAI.SKGap.FullMain.varianceEnergy_eq line 34
4. lemma OAI.SKGap.FullMain.fieldGibbs_prior line 52
5. lemma OAI.SKGap.FullMain.covariance_square_bound line 56
6. lemma OAI.SKGap.FullMain.squareMean_eq line 71
7. lemma OAI.SKGap.FullMain.squareMean_one line 74
8. lemma OAI.SKGap.FullMain.energy_one line 79
9. lemma OAI.SKGap.FullMain.stable_mean_difference line 88
10. lemma OAI.SKGap.FullMain.drift_square_of_stable_mean line 114
11. lemma OAI.SKGap.FullMain.gaussianChannelLaw_step line 150
12. lemma OAI.SKGap.FullMain.history_field_event line 164
13. lemma OAI.SKGap.FullMain.measurable_rootFields line 178
14. lemma OAI.SKGap.FullMain.history_root_probability line 186
15. lemma OAI.SKGap.FullMain.history_terminal_probability line 220