OAI/NumberTheory/Ostmann/ZeroDensity/SmoothMellinInversion.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Mellin inversion for the concrete prime-mean test

  1. def OAI.Ostmann.complexPrimeMeanTest line 14
  2. theorem OAI.Ostmann.complexPrimeMeanTest_continuous line 16
  3. theorem OAI.Ostmann.primeMeanMellin_eq_mellin line 19
  4. theorem OAI.Ostmann.complexPrimeMeanTest_bigO_atTop line 30
  5. theorem OAI.Ostmann.complexPrimeMeanTest_bigO_zero line 37
  6. theorem OAI.Ostmann.primeMeanMellin_differentiable line 45
  7. theorem OAI.Ostmann.complexPrimeMeanTest_mellinConvergent line 53
  8. theorem OAI.Ostmann.primeMeanMellin_verticalIntegrable line 60
  9. theorem OAI.Ostmann.primeMeanTest_mellin_inversion line 72

    Source documentation

    Inversion on Re(s)=2, used before shifting the explicit-formula contour.

    theorem primeMeanTest_mellin_inversion (x : ℝ) (hx : 0 < x) :
    mellinInv 2 primeMeanMellin x = (primeMeanTest x : ℂ) := by
…

    Mentions: OAI.Ostmann.primeMeanMellin, OAI.Ostmann.primeMeanTest