OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/HasDerivAtLogPrimitive.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryLogIntegral.hasDerivAt_logPrimitive line 12
2. lemma OAI.OrdinaryLogIntegral.hasDerivAt_logSecond line 22
3. lemma OAI.OrdinaryLogIntegral.intervalIntegrable_logPhase line 32
4. theorem OAI.OrdinaryLogIntegral.linear_log_integral line 39
5. def OAI.OrdinaryLogIntegral.triangleMellin line 70
6. theorem OAI.OrdinaryLogIntegral.triangleMellin_identity line 74
7. lemma OAI.OrdinaryLogIntegral.norm_mellin_denominator line 86
8. theorem OAI.OrdinaryLogIntegral.triangleMellin_bound line 101