OAI/NumberTheory/GaussianMoat/GroupCoverage.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GaussianMoat.overlapCount line 13
2. lemma OAI.GaussianMoat.overlapCount_sum line 16
3. def OAI.GaussianMoat.overlapExceptions line 28
4. lemma OAI.GaussianMoat.overlapExceptions_card line 31
5. lemma OAI.GaussianMoat.coverage_hit_lower line 51
6. def OAI.GaussianMoat.coverageList line 112
7. theorem OAI.GaussianMoat.coverageList_tail line 117
8. lemma OAI.GaussianMoat.FinLaw.prod_ite_forall line 195
9. lemma OAI.GaussianMoat.FinLaw.iid_map line 204
10. lemma OAI.GaussianMoat.FinLaw.iid_prob_forall line 215
11. lemma OAI.GaussianMoat.FinLaw.iid_prob_implies line 228
12. lemma OAI.GaussianMoat.FinLaw.iid_survival_exp line 234
13. lemma OAI.GaussianMoat.FinLaw.expect_map line 245
14. lemma OAI.GaussianMoat.FinLaw.joint_expect_snd line 254
15. lemma OAI.GaussianMoat.FinLaw.prob_map_true line 258
16. lemma OAI.GaussianMoat.FinLaw.prob_le_of_expect line 262
17. lemma OAI.GaussianMoat.FinLaw.H_sub_H_of_agree line 276
18. lemma OAI.GaussianMoat.FinLaw.condH_sub_condH_of_agree line 288
19. lemma OAI.GaussianMoat.FinLaw.binEntropy_le_log_inverse line 304
20. lemma OAI.GaussianMoat.FinLaw.binEntropy_sum_le line 321
21. lemma OAI.GaussianMoat.FinLaw.prob_mem_finset line 333
22. lemma OAI.GaussianMoat.FinLaw.joint_prob_le_bad_add line 347
23. lemma OAI.GaussianMoat.FinLaw.iid_true_hit_expect line 367
24. lemma OAI.GaussianMoat.FinLaw.true_coverageList_probability line 392
25. lemma OAI.GaussianMoat.FinLaw.coverageList_size_probability line 418