OAI/NumberTheory/Ostmann/Arithmetic/OpenCellPrimeComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.complexPrimeInterval_open_cell_bound line 12
2. theorem OAI.Ostmann.PublishedProgressionInput.open_cell_prime_comparison line 33

   Source documentation

   A cell's interior uses its continuous smooth factor; the right endpoint is accounted for by its prime atom, even when it is an arithmetic root.

   theorem PublishedProgressionInput.open_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)
       (W w : ℝ → ℂ) (hwc : ContinuousOn w (Set.Icc u v)) (V B : ℝ)
       (hV : ∀ s : ℕ → ℝ, Monotone s → ∀ N, s 0 = u → s N = v →
         discreteVariation (fun j => w (s j)) N ≤ V)
       (hB : 0 ≤ B) (hbound : ∀ y ∈ Set.Ioc u v, ‖W y - w y‖ ≤ B)
       (heq : ∀ y ∈ Set.Ioo u v, W y = w y) :
       ‖complexPrimeInterval q a u v W -
         ∫ y in Set.Ioc u v, w y * (selectedPrimeLogDensity P Q q a y : ℂ)‖ ≤
         V * (18 * P.errorConstant * Real.exp (-P.decay * Real.sqrt u) +
           Real.exp (-P.kappa * u / Real.log (4 * (Q : ℝ)))) + B * Real.exp (-u) := by
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.discreteVariation, OAI.Ostmann.complexPrimeInterval, OAI.Ostmann.selectedPrimeLogDensity

3. theorem OAI.Ostmann.PublishedProgressionInput.piecewise_prime_comparison line 52

   Source documentation

   Sum the actual prime weights over the constructed root partition. The ideal term is the sum of its continuous cell integrals with the Page factor.

   theorem PublishedProgressionInput.piecewise_prime_comparison (P : PublishedProgressionInput)
       {Q q a : ℕ} (hQ : 2 ≤ Q) (hq : 1 ≤ q) (hqQ : q ≤ Q) (ha : a.Coprime q)
       (s : ℕ → ℝ) (hs : Monotone s) (N : ℕ) (hs0 : 1 ≤ s 0) (hshort : s N ≤ s 0 + 1)
       (W : ℝ → ℂ) (w : ℕ → ℝ → ℂ) (V B : ℕ → ℝ)
       (hwc : ∀ j < N, ContinuousOn (w j) (Set.Icc (s j) (s (j + 1))))
       (hV : ∀ j < N, ∀ r : ℕ → ℝ, Monotone r → ∀ M,
         r 0 = s j → r M = s (j + 1) → discreteVariation (fun k => w j (r k)) M ≤ V j)
       (hB : ∀ j < N, 0 ≤ B j)
       (hbound : ∀ j < N, ∀ y ∈ Set.Ioc (s j) (s (j + 1)), ‖W y - w j y‖ ≤ B j)
       (heq : ∀ j < N, ∀ y ∈ Set.Ioo (s j) (s (j + 1)), W y = w j y) :
       ‖complexPrimeInterval q a (s 0) (s N) W -
         ∑ j ∈ Finset.range N, ∫ y in Set.Ioc (s j) (s (j + 1)),
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.discreteVariation, OAI.Ostmann.complexPrimeInterval