OAI/NumberTheory/Ostmann/Arithmetic/RootMeshIntegral.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.rootMeshWeight_integral line 11
2. theorem OAI.Ostmann.PublishedProgressionInput.common_root_prime_integral line 53

   Source documentation

   No root-dependent main term survives the partition. The full density and the sharp real gate remain inside one integral.

   theorem PublishedProgressionInput.common_root_prime_integral (P : PublishedProgressionInput)
       (S : Finset ℝ) (s : ℕ → ℝ) (hs : Monotone s) (N : ℕ)
       (hfree : ∀ j < N, ∀ r ∈ S, r ∉ Set.Ioo (Real.exp (s j)) (Real.exp (s (j + 1))))
       {Q q a : ℕ} (hQ : 2 ≤ Q) (hq : 1 ≤ q) (hqQ : q ≤ Q) (ha : a.Coprime q)
       (hu : 1 ≤ s 0) (hshort : s N ≤ s 0 + 1)
       {k : ℕ} (F : Fin k → ClippedPolynomialFactor)
       (hroots : ∀ i r, r ∈ (F i).polynomial.derivative.roots → r ∈ S)
       (w : ℝ → ℂ) (C : ℝ) (hC : 0 ≤ C) (hw : ∀ x, ‖w x‖ ≤ C)
       (hconst : ∀ x y, rootCellCode S x = rootCellCode S y → w x = w y) :
       ‖complexPrimeInterval q a (s 0) (s N)
           (fun y => w (Real.exp y) * smoothPolynomialWeight F (Real.exp y)) -
         ∫ y in Set.Ioc (s 0) (s N), w (Real.exp y) * smoothPolynomialWeight F (Real.exp y) *
   …

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

3. theorem OAI.Ostmann.common_root_integer_integral line 77