OAI/NumberTheory/ShortEgyptian/HammingDistance.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ShortEgyptian.hammingDistance line 13
2. lemma OAI.ShortEgyptian.hamming_weight line 16
3. lemma OAI.ShortEgyptian.hamming_moment line 21
4. lemma OAI.ShortEgyptian.hamming_tail line 29
5. lemma OAI.ShortEgyptian.hamming_tail_exp line 45
6. lemma OAI.ShortEgyptian.complex_expect_re line 62
7. lemma OAI.ShortEgyptian.complex_expect_norm_sq line 74
8. lemma OAI.ShortEgyptian.mean_square_correlation_bound line 83