OAI/NumberTheory/Ostmann/Arithmetic/WeightedPrimeIntervals.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.weightedReciprocalPrimeInterval line 12
2. theorem OAI.Ostmann.log_mem_of_mem_exp_interval line 17
3. theorem OAI.Ostmann.reciprocalPrimeInterval_nonneg line 26
4. theorem OAI.Ostmann.weightedReciprocalPrimeInterval_freeze line 34

   Source documentation

   Freezing uses the actual prime weights, with no equidistribution or independence hypothesis.

   theorem weightedReciprocalPrimeInterval_freeze (q a : ℕ) (s t : ℝ)
       (w : ℝ → ℝ) (w₀ η : ℝ)
       (hw : ∀ y ∈ Set.Ioc s t, |w y - w₀| ≤ η) :
       |weightedReciprocalPrimeInterval q a s t w -
         w₀ * reciprocalPrimeInterval q a (Real.exp s) (Real.exp t)| ≤
         η * reciprocalPrimeInterval q a (Real.exp s) (Real.exp t) := by
   …

   Mentions: OAI.Ostmann.weightedReciprocalPrimeInterval, OAI.Ostmann.reciprocalPrimeInterval

5. theorem OAI.Ostmann.primeLogDensity_abs_le_two line 64
6. theorem OAI.Ostmann.primeLogDensity_integral_abs_le_two line 72
7. theorem OAI.Ostmann.primeLogDensity_integral_freeze line 86
8. theorem OAI.Ostmann.weighted_prime_log_interval_error line 121

   Source documentation

   Transfer a bare progression estimate to the actual cutoff-weighted prime cell. The cutoff variation is controlled independently of its sign.

   theorem weighted_prime_log_interval_error (q a : ℕ) (φ χ β : ℝ)
       (hφ : 1 ≤ φ) (hχ : |χ| ≤ 1) (hβ : β ≤ 1) {s t : ℝ}
       (hs : 1 ≤ s) (hst : s ≤ t) (hshort : t ≤ s + 1)
       (w : ℝ → ℝ) (hwc : ContinuousOn w (Set.Icc s t)) (w₀ η δ : ℝ) (hη : 0 ≤ η)
       (hw : ∀ y ∈ Set.Ioc s t, |w y - w₀| ≤ η)
       (hbare : |reciprocalPrimeInterval q a (Real.exp s) (Real.exp t) -
         ∫ y in Set.Ioc s t, primeLogDensity φ χ β y| ≤ δ) :
       |weightedReciprocalPrimeInterval q a s t w -
         ∫ y in Set.Ioc s t, w y * primeLogDensity φ χ β y| ≤
         (|w₀| + η) * δ + 4 * η := by
   …

   Mentions: OAI.Ostmann.reciprocalPrimeInterval, OAI.Ostmann.primeLogDensity, OAI.Ostmann.weightedReciprocalPrimeInterval