OAI/NumberTheory/Ostmann/Arithmetic/CommonRootMesh.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.rootMeshWeight line 12
2. theorem OAI.Ostmann.rootMeshWeight_continuous line 16
3. theorem OAI.Ostmann.rootMeshWeight_variation line 20
4. theorem OAI.Ostmann.rootMeshWeight_bound line 43
5. theorem OAI.Ostmann.rootMeshWeight_eq line 58
6. theorem OAI.Ostmann.PublishedProgressionInput.common_root_mesh_prime_comparison line 74

   Source documentation

   The mesh is supplied before the residue class and coefficient.

   theorem PublishedProgressionInput.common_root_mesh_prime_comparison (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)) -
         ∑ j ∈ Finset.range N, ∫ y in Set.Ioc (s j) (s (j + 1)),
   …

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

7. theorem OAI.Ostmann.common_root_mesh_integer_comparison line 100