OAI/NumberTheory/GaussianMoat/PosteriorSampling.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GaussianMoat.FinLaw.prob_and_split line 13
2. lemma OAI.GaussianMoat.FinLaw.prob_mix line 20
3. lemma OAI.GaussianMoat.FinLaw.posterior_unfavorable line 24
4. lemma OAI.GaussianMoat.FinLaw.mixed_exception_card line 31
5. lemma OAI.GaussianMoat.FinLaw.mixed_floor line 79
6. lemma OAI.GaussianMoat.FinLaw.prob_exists_eq_sum_disjoint line 103
7. lemma OAI.GaussianMoat.FinLaw.Hf_id line 131
8. lemma OAI.GaussianMoat.FinLaw.cHf_joint_fst line 133
9. lemma OAI.GaussianMoat.FinLaw.joint_iid_eval line 143
10. theorem OAI.GaussianMoat.FinLaw.conditional_iid_information line 150
11. def OAI.GaussianMoat.FinLaw.passingList line 185
12. lemma OAI.GaussianMoat.FinLaw.expect_card_passingList line 188
13. lemma OAI.GaussianMoat.FinLaw.passingList_true line 220
14. lemma OAI.GaussianMoat.FinLaw.expect_log_le_log_expect line 232
15. lemma OAI.GaussianMoat.FinLaw.expected_log_card_passingList line 245
16. lemma OAI.GaussianMoat.FinLaw.conditional_passing_support line 265
17. lemma OAI.GaussianMoat.FinLaw.cHf_prefix_step line 281
18. lemma OAI.GaussianMoat.FinLaw.cHf_blocks_le line 310