OAI/NumberTheory/Ostmann/Arithmetic/RootCellPrimeComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.PublishedProgressionInput.root_cell_prime_comparison line 15

   Source documentation

   Root-cell multipliers include the exact sharp arithmetic indicators. The continuous factors and all endpoint primes are retained.

   theorem PublishedProgressionInput.root_cell_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)
       {n : ℕ} (F : Fin n → ClippedPolynomialFactor)
       (S : Finset ℝ) (hroots : ∀ i r, r ∈ (F i).polynomial.derivative.roots → r ∈ S)
       (c : (S → Ordering) → ℂ) (C : ℝ) (hC : 0 ≤ C) (hc : ∀ code, ‖c code‖ ≤ C) :
       ∃ (s : ℕ → ℝ) (N : ℕ) (d : ℕ → ℂ),
         Monotone s ∧ s 0 = u ∧ s N = v ∧ N ≤ S.card + 1 ∧ (∀ j, ‖d j‖ ≤ C) ∧
         ‖complexPrimeInterval q a u v
             (fun y => c (rootCellCode S (Real.exp y)) * smoothPolynomialWeight F (Real.exp y)) -
           ∑ j ∈ Finset.range N, ∫ y in Set.Ioc (s j) (s (j + 1)),
             d j * smoothPolynomialWeight F (Real.exp y) *
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.ClippedPolynomialFactor, OAI.Ostmann.complexPrimeInterval, OAI.Ostmann.rootCellCode, OAI.Ostmann.smoothPolynomialWeight