OAI/NumberTheory/Ostmann/ZeroDensity/SmoothPrincipalPartialSummation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The fixed principal-character mean by partial summation

This identifies the literal smooth mean with a compactly supported integral of the Chebyshev function, for use with the quantitative PNT.

  1. theorem OAI.Ostmann.primeMeanTest_deriv_continuous line 20
  2. theorem OAI.Ostmann.primeMeanTest_deriv_zero_outside line 23
  3. theorem OAI.Ostmann.primeMeanTest_deriv_bound line 32
  4. theorem OAI.Ostmann.scaledPrimeMeanTest_hasDerivAt line 45
  5. theorem OAI.Ostmann.smoothPrincipalMean_eq_real_sum line 52
  6. theorem OAI.Ostmann.smoothPrincipalMean_partial_summation line 70
  7. theorem OAI.Ostmann.primeMeanTest_integral_unit line 94
  8. theorem OAI.Ostmann.scaledPrimeMean_main_integral line 103
  9. theorem OAI.Ostmann.scaledPrimeMean_psi_integrable line 122
  10. theorem OAI.Ostmann.smoothPrincipalError_integral line 133

    Source documentation

    The exact principal error is the integral of the unsmoothed PNT error.

    theorem smoothPrincipalError_integral (X : ℝ) (hX : 0 < X) :
    smoothPrincipalError X =
      |∫ t in (0 : ℝ)..X, deriv primeMeanTest (t / X) / X *
        (Chebyshev.psi t - t)| := by
…

    Mentions: OAI.Ostmann.smoothPrincipalError, OAI.Ostmann.primeMeanTest