OAI/NumberTheory/Ostmann/ZeroDensity/ArithmeticProgressionRows.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.Ostmann.ArithmeticProgressionRow line 11
2. def OAI.Ostmann.ArithmeticProgressionRow.leftExponent line 18
3. def OAI.Ostmann.ArithmeticProgressionRow.modulusExponent line 22
4. def OAI.Ostmann.ArithmeticProgressionRow.errorExponent line 26
5. theorem OAI.Ostmann.ArithmeticProgressionRow.gaps line 30
6. theorem OAI.Ostmann.PublishedProgressionInput.row_log_interval line 42

   Source documentation

   Exactly the two rows of the manuscript's progression table, with one exceptional character for all moduli in the row. The logarithmic interval estimate is proved from the published theta and Page inputs.

   theorem PublishedProgressionInput.row_log_interval (P : PublishedProgressionInput)
       (r : ArithmeticProgressionRow) :
       ∀ᶠ L : ℝ in atTop, ∀ (q Q a : ℕ), 2 ≤ Q → 1 ≤ q → q ≤ Q → a.Coprime q →
         Real.log (Q : ℝ) ≤ Real.exp (r.modulusExponent * L) →
         ∀ s t : ℝ, 1 ≤ s → Real.exp (r.leftExponent * 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 (r.errorExponent * L)) := by
   …

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