ProgressionErrorRates.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The two arithmetic progression precision scales

The published square-root-log theta error is sufficient on both rows of Section 8. The discarded Page zeros have the stronger exponent a₀ - μ.

theorem OAI.Ostmann.constant_mul_double_exp_le line 16
theorem OAI.Ostmann.sqrt_ge_log_scale line 30
theorem OAI.Ostmann.page_gap_ge_log_scale line 36

theorem OAI.Ostmann.PublishedProgressionInput.log_interval_rate line 55

Source documentation

Uniform in the modulus, residue and endpoints. The factor two is an absolute constant, and no upper endpoint scale is required.

theorem PublishedProgressionInput.log_interval_rate (P : PublishedProgressionInput)
    (a₀ μ δ : ℝ) (ha : 0 < a₀) (hδa : δ < a₀ / 2) (hδμ : δ < a₀ - μ)
    (haμ : 0 < a₀ - μ) :
    ∀ᶠ L : ℝ in atTop, ∀ (q Q a : ℕ), 2 ≤ Q → 1 ≤ q → q ≤ Q → a.Coprime q →
      Real.log (4 * (Q : ℝ)) ≤ 2 * Real.exp (μ * L) →
      ∀ s t : ℝ, 1 ≤ s → Real.exp (a₀ * L) ≤ s → s ≤ t → t ≤ s + 1 →
      |reciprocalPrimeInterval q a (Real.exp s) (Real.exp t) -
        ∫ y in Set.Ioc s t, primeLogDensity (Nat.totient q)
          (pageCoefficient (pageAtModulus q (selectedPageZero P Q)) a)
          (pageBeta (pageAtModulus q (selectedPageZero P Q))) y| ≤
        2 * Real.exp (-Real.exp (δ * L)) := by
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.reciprocalPrimeInterval, OAI.Ostmann.primeLogDensity, OAI.Ostmann.pageCoefficient, OAI.Ostmann.pageAtModulus, OAI.Ostmann.selectedPageZero, OAI.Ostmann.pageBeta