OAI/NumberTheory/GaussianMoat/BackwardCoverage.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GaussianMoat.FinLaw.short_list_probability_deficit line 12
2. lemma OAI.GaussianMoat.FinLaw.average_deficit_lower line 30
3. theorem OAI.GaussianMoat.FinLaw.shared_coverage_deficit line 59
4. lemma OAI.GaussianMoat.perm_expect_apply line 90
5. lemma OAI.GaussianMoat.FinLaw.Hf_sub_le_cHf line 108
6. lemma OAI.GaussianMoat.FinLaw.orderedEntropy_conditioning line 114
7. lemma OAI.GaussianMoat.FinLaw.signedEntropy_conditioning line 139
8. theorem OAI.GaussianMoat.SplitSieve.coverage_conditioning line 150
9. theorem OAI.GaussianMoat.FinLaw.backward_coverage_step line 162
10. theorem OAI.GaussianMoat.FinLaw.low_mass_average line 246
11. lemma OAI.GaussianMoat.FinLaw.uniform_map_perm line 279
12. lemma OAI.GaussianMoat.FinLaw.prob_uniform line 284
13. lemma OAI.GaussianMoat.FinLaw.uniform_no_wrap line 293
14. lemma OAI.GaussianMoat.FinLaw.joint_perm_second line 315
15. lemma OAI.GaussianMoat.FinLaw.smoothing_prob line 321
16. lemma OAI.GaussianMoat.FinLaw.smoothing_condH line 350