OAI/NumberTheory/ShortEgyptian/SamplePartitions.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ShortEgyptian.mergeSamples line 13
2. def OAI.ShortEgyptian.partitionSamples line 18
3. lemma OAI.ShortEgyptian.expect_partition line 36
4. lemma OAI.ShortEgyptian.prod_partition line 52
5. lemma OAI.ShortEgyptian.prod_mergeSamples line 59
6. def OAI.ShortEgyptian.normalizeSamples line 75
7. lemma OAI.ShortEgyptian.expect_normalize line 83
8. lemma OAI.ShortEgyptian.uniform_prime_bilinear_two line 94