OAI/NumberTheory/Ostmann/Construction/PrimeCutoffFactors.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.primeCutoffFactors line 15

   Source documentation

   The extra factor is the original top-prime cell cutoff, evaluated in the same positive real coordinate as the history polynomials.

   noncomputable def primeCutoffFactors {n : ℕ} (F : Fin n → ClippedPolynomialFactor)
       (φ : ℝ → ℝ) (G B D : ℝ) (hB : 0 ≤ B) (hD : 0 ≤ D)
       (hφ : ∀ x, |φ x| ≤ B) (hlip : ∀ x y, |φ x - φ y| ≤ D * |x - y|) :
       Fin (n + 1) → ClippedPolynomialFactor :=
   …

   Mentions: OAI.Ostmann.ClippedPolynomialFactor

2. theorem OAI.Ostmann.primeCutoffFactors_value line 21
3. theorem OAI.Ostmann.primeCutoffFactors_budget line 33
4. theorem OAI.Ostmann.primeCutoffFactors_roots line 43
5. theorem OAI.Ostmann.PublishedProgressionInput.cutoff_smooth_prime_comparison line 57

   Source documentation

   The original harmonic prior's smooth cutoff is retained in the actual prime sum and in the Page integral. Its cost is independent of the cell center.

   theorem PublishedProgressionInput.cutoff_smooth_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)
       (hcode : rootCellCode S (Real.exp u) = rootCellCode S (Real.exp v))
       (φ : ℝ → ℝ) (G B D : ℝ) (hB : 0 ≤ B) (hD : 0 ≤ D)
       (hφ : ∀ x, |φ x| ≤ B) (hlip : ∀ x y, |φ x - φ y| ≤ D * |x - y|)
       (hout : ∀ x, 1 ≤ |x| → φ x = 0) :
       ‖complexPrimeInterval q a u v (fun y => (φ (y - G) : ℂ) * smoothPolynomialWeight F (Real.exp y)) -
         ∫ y in Set.Ioc u v, ((φ (y - G) : ℂ) * smoothPolynomialWeight F (Real.exp y)) *
           (selectedPrimeLogDensity P Q q a y : ℂ)‖ ≤
   …

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