OAI/NumberTheory/Ostmann/Arithmetic/MovingSmoothPrimeComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.moving_smooth_prime_comparison line 15

   Source documentation

   The actual moving Fourier leaves and all logarithmic node cutoffs have one uniform prime-to-Page comparison. The cut set has at most one derivative root per leaf; the error contains no mesh count and no node-center factor.

   theorem moving_smooth_prime_comparison {σ : Type*} (value : σ → ℕ)
       {n : ℕ} (T : MovingSlotData σ n) (L R : Polynomial ℝ) (ψ : 𝓢(ℝ, ℂ))
       (X lo hi V : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi)
       (hL : L.natDegree ≤ 1) (hR : R.natDegree ≤ 1)
       (hV : T.Frequencies (fun s => |(s : ℝ)| ≤ V)) (φ : ℝ → ℝ)
       (G : ℕ → ℝ) (B D : ℝ) (hB : 0 ≤ B) (hD : 0 ≤ D)
       (hφ : ∀ x, |φ x| ≤ B) (hlip : ∀ x y, |φ x - φ y| ≤ D * |x - y|) :
       ∃ S : Finset ℝ, S.card ≤ 2 ^ n ∧
         ∀ (P : PublishedProgressionInput) (Q q a : ℕ),
         2 ≤ Q → 1 ≤ q → q ≤ Q → a.Coprime q →
         ∀ u v : ℝ, 1 ≤ u → u ≤ v → v ≤ u + 1 →
         rootCellCode S (Real.exp u) = rootCellCode S (Real.exp v) →
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.rootCellCode