OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/WeightedPartialSumBound.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryLogIntegral.weighted_partial_sum_bound line 14
2. lemma OAI.OrdinaryLogIntegral.logPhase_mul line 40
3. lemma OAI.OrdinaryLogIntegral.tentPhase_eq line 47
4. lemma OAI.OrdinaryLogIntegral.weighted_logPhase_bound line 54
5. def OAI.OrdinaryLogIntegral.differencingBudget line 76
6. lemma OAI.OrdinaryLogIntegral.differencingBudget_nonneg line 80
7. lemma OAI.OrdinaryLogIntegral.differencingBudget_mono line 84
8. lemma OAI.OrdinaryLogIntegral.partial_logphase_bound line 90
9. theorem OAI.OrdinaryLogIntegral.weighted_discrete_logphase line 100