ContinuousPrimeComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Comparing the full continuous weight with the retained Page measure

theorem OAI.Ostmann.PublishedProgressionInput.continuous_prime_comparison line 12

Source documentation

A continuous weight with a uniform variation budget can be used directly in the published progression estimate. No mesh parameter survives.

theorem PublishedProgressionInput.continuous_prime_comparison (P : PublishedProgressionInput)
    {Q q a : ℕ} (hQ : 2 ≤ Q) (hq : 1 ≤ q) (hqQ : q ≤ Q) (ha : a.Coprime q)
    (u v : ℝ) (hu : 1 ≤ u) (huv : u ≤ v) (hshort : v ≤ u + 1)
    (w : ℝ → ℂ) (hwc : ContinuousOn w (Set.Icc u v)) (V : ℝ)
    (hV : ∀ (s : ℕ → ℝ), Monotone s → ∀ N, s 0 = u → s N = v →
      discreteVariation (fun j => w (s j)) N ≤ V) :
    ‖complexPrimeInterval q a u v w -
        ∫ y in Set.Ioc u v, w y * (selectedPrimeLogDensity P Q q a y : ℂ)‖ ≤
      V * (18 * P.errorConstant * Real.exp (-P.decay * Real.sqrt u) +
        Real.exp (-P.kappa * u / Real.log (4 * (Q : ℝ)))) := by
…

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