OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/PowersetFirstMoment.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryWindowEuler.powerset_first_moment line 21
2. lemma OAI.OrdinaryWindowEuler.truncated_mass line 45
3. def OAI.OrdinaryWindowEuler.primeWeight line 74
4. lemma OAI.OrdinaryWindowEuler.prime_weight_nonneg line 76
5. lemma OAI.OrdinaryWindowEuler.prime_weight_moment line 81
6. lemma OAI.OrdinaryWindowEuler.log_prod_primes line 91
7. theorem OAI.OrdinaryWindowEuler.truncated_prime_mass line 97
8. lemma OAI.OrdinaryWindowEuler.prime_log_mass line 122