OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/Complete.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryLogDerivative.Complete line 19
2. def OAI.OrdinaryLogDerivative.mangoldtTwist line 22
3. lemma OAI.OrdinaryLogDerivative.twist_convolution line 25
4. lemma OAI.OrdinaryLogDerivative.mangoldt_convolution line 37
5. lemma OAI.OrdinaryLogDerivative.mangoldt_summable line 47
6. theorem OAI.OrdinaryLogDerivative.LSeries_derivative_product line 57
7. theorem OAI.OrdinaryLogDerivative.log_weighted_sum line 67