OAI/NumberTheory/Ostmann/Arithmetic/PrimeHarmonicError.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.primeHarmonic_error_le line 13

   Source documentation

   Partial summation loses only endpoint weights and the variation of the harmonic weight. The theta estimate is used on exactly this interval.

   theorem primeHarmonic_error_le (q a : ℕ) (φ χ β : ℝ) (hβ : β ≠ 0)
       {u v : ℝ} (hu : 1 < u) (huv : u ≤ v)
       (E B D : ℝ) (hB : 0 ≤ B) (hD : 0 ≤ D)
       (hθ : ∀ t ∈ Set.Icc u v, |primeProgressionTheta q a t - thetaMainTerm φ χ β t| ≤ E)
       (hf : ∀ t ∈ Set.Icc u v, |primeHarmonicWeight t| ≤ B)
       (hdf : ∀ t ∈ Set.Icc u v, |primeHarmonicDerivative t| ≤ D) :
       |reciprocalPrimeInterval q a u v -
         ∫ t in Set.Ioc u v, primeHarmonicWeight t * thetaMainDensity φ χ β t| ≤
           E * (2 * B + (v - u) * D) := by
   …

   Mentions: OAI.Ostmann.primeProgressionTheta, OAI.Ostmann.thetaMainTerm, OAI.Ostmann.primeHarmonicWeight, OAI.Ostmann.primeHarmonicDerivative, OAI.Ostmann.reciprocalPrimeInterval, OAI.Ostmann.thetaMainDensity