OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/SumIntegralError.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.OrdinaryLogIntegral.sum_integral_error line 11
  2. def OAI.OrdinaryLogIntegral.logPhase line 66
  3. lemma OAI.OrdinaryLogIntegral.norm_logPhase line 68
  4. lemma OAI.OrdinaryLogIntegral.hasDerivAt_logPhase line 71
  5. def OAI.OrdinaryLogIntegral.differencePhase line 77
  6. lemma OAI.OrdinaryLogIntegral.norm_differencePhase line 80
  7. lemma OAI.OrdinaryLogIntegral.hasDerivAt_differencePhase line 83
  8. lemma OAI.OrdinaryLogIntegral.differencePhase_eq line 100
  9. lemma OAI.OrdinaryLogIntegral.hasDerivAt_differenceMultiplier line 108
  10. theorem OAI.OrdinaryLogIntegral.difference_integral_bound line 123
  11. theorem OAI.OrdinaryLogIntegral.difference_sum_integral_error line 177
  12. theorem OAI.OrdinaryLogIntegral.difference_sum_bound line 194