OAI/Geometry/TranslativeCovering/TargetSampling.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TargetSampling.pair_preserving line 41
2. def OAI.TargetSampling.pairs line 53
3. def OAI.TargetSampling.score line 56
4. lemma OAI.TargetSampling.score_nonneg line 60
5. lemma OAI.TargetSampling.score_integrable line 65
6. lemma OAI.TargetSampling.score_integral line 76
7. lemma OAI.TargetSampling.score_ge_one line 98
8. lemma OAI.TargetSampling.ae_distinct line 106
9. lemma OAI.TargetSampling.ae_in_set line 127
10. theorem OAI.TargetSampling.select line 137