OAI/Probability/SKGap/Posterior/GOEObservation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.goeObservation line 13
2. def OAI.SKGap.observationCoeff line 16
3. lemma OAI.SKGap.observationCoeff_sample line 19
4. lemma OAI.SKGap.goe_observation_joint_gaussian line 38
5. lemma OAI.SKGap.goe_noise_cov line 52
6. lemma OAI.SKGap.goe_mulVec_memLp line 63
7. lemma OAI.SKGap.goe_entry_observation_cov line 69
8. lemma OAI.SKGap.goe_mulVec_noise_cov line 85
9. lemma OAI.SKGap.goe_mulVec_cov line 104
10. lemma OAI.SKGap.goe_observation_mean line 124
11. lemma OAI.SKGap.goe_observation_cov line 129