OAI/NumberTheory/Ostmann/Arithmetic/PrimePartitionVariation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.complexPrimeInterval_partition line 11
2. theorem OAI.Ostmann.reciprocalPrimeInterval_partition line 21
3. theorem OAI.Ostmann.integral_Ioc_partition line 31
4. theorem OAI.Ostmann.PublishedProgressionInput.prime_partition_variation line 50

   Source documentation

   The oscillation error is proportional to total mass and total interval length. The progression error is proportional to variation, with neither error multiplied by the number of intervals.

   theorem PublishedProgressionInput.prime_partition_variation (P : PublishedProgressionInput)
       {Q q a : ℕ} (hQ : 2 ≤ Q) (hq : 1 ≤ q) (hqQ : q ≤ Q) (ha : a.Coprime q)
       (s : ℕ → ℝ) (hs : Monotone s) (hs0 : 1 ≤ s 0) (N : ℕ) (hshort : s N ≤ s 0 + 1)
       (w : ℝ → ℂ) (hwc : ContinuousOn w (Set.Icc (s 0) (s N))) (η : ℝ) (hη : 0 ≤ η)
       (hw : ∀ j < N, ∀ y ∈ Set.Ioc (s j) (s (j + 1)), ‖w y - w (s j)‖ ≤ η) :
       ‖complexPrimeInterval q a (s 0) (s N) w -
           ∫ y in Set.Ioc (s 0) (s N), w y * (selectedPrimeLogDensity P Q q a y : ℂ)‖ ≤
         discreteVariation (fun j => w (s j)) N *
           (18 * P.errorConstant * Real.exp (-P.decay * Real.sqrt (s 0)) +
             Real.exp (-P.kappa * s 0 / Real.log (4 * (Q : ℝ)))) +
         η * (reciprocalPrimeInterval q a (Real.exp (s 0)) (Real.exp (s N)) +
           2 * (s N - s 0)) := by
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.complexPrimeInterval, OAI.Ostmann.selectedPrimeLogDensity, OAI.Ostmann.discreteVariation, OAI.Ostmann.reciprocalPrimeInterval