OAI/NumberTheory/Ostmann/ZeroDensity/ThetaMainTerm.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The exceptional theta term and its harmonic density

Differentiating the published theta main term cancels its factor β. The corresponding harmonic density is retained exactly.

  1. def OAI.Ostmann.thetaMainTerm line 17
  2. def OAI.Ostmann.thetaMainDensity line 20
  3. theorem OAI.Ostmann.hasDerivAt_thetaMainTerm line 23
  4. theorem OAI.Ostmann.continuousOn_thetaMainDensity line 38
  5. theorem OAI.Ostmann.thetaMain_harmonic_integral line 45