OAI/NumberTheory/ShortEgyptian/ProductCorrelations.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ShortEgyptian.sampleProduct line 13
2. lemma OAI.ShortEgyptian.pair_exposure_identity line 16
3. lemma OAI.ShortEgyptian.pair_correlation_bound line 68
4. lemma OAI.ShortEgyptian.disjoint_subsets_card line 140
5. lemma OAI.ShortEgyptian.mean_square_correlation_exp line 150