OAI/NumberTheory/Ostmann/Arithmetic/RealBulkPrimeComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.realBulkPrimeSmoothSum line 11
2. theorem OAI.Ostmann.realBulkPrimeSmoothSum_polynomial line 19
3. theorem OAI.Ostmann.PublishedProgressionInput.real_bulk_prime_comparison line 43

   Source documentation

   The same comparison allows arbitrary real values in every other bulk slot. The real integral is the polynomial extension proved equal to the original sampling expression at every prime, with all endpoint primes retained.

   theorem PublishedProgressionInput.real_bulk_prime_comparison (P : PublishedProgressionInput)
       {σ : Type*} (value : σ → ℝ) (i : σ) {n : ℕ} (T : MovingSlotData σ n)
       (hT : T.CompensationAbsent i) (L R : Polynomial ℝ) (ψ : 𝓢(ℝ, ℂ))
       (X lo hi V : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi)
       (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|)
       (hout : ∀ x, 1 ≤ |x| → φ x = 0)
       (d r e : ℕ) (hsize : T.SizeLE d) (hregular : T.RegularLengthLE r)
       (hL : L.natDegree ≤ e) (hR : R.natDegree ≤ e)
       {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) :
   …

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