OAI/NumberTheory/Ostmann/Arithmetic/BulkPairPrimeComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.realValueSmoothPair line 12
2. def OAI.Ostmann.bulkPairComparisonBudget line 18
3. theorem OAI.Ostmann.PublishedProgressionInput.bulk_pair_prime_comparison line 25

   Source documentation

   Both trees retain their actual shared bulk coordinate. Conjugation doubles the root budget and squares the smooth budget, without any new analytic input.

   theorem PublishedProgressionInput.bulk_pair_prime_comparison (P : PublishedProgressionInput)
       {σ : Type*} (value : σ → ℝ) (i : σ) {n : ℕ} (T : Bool → MovingSlotData σ n)
       (hT : ∀ b, (T b).CompensationAbsent i) (L R : Polynomial ℝ) (ψ : 𝓢(ℝ, ℂ))
       (X lo hi V : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi)
       (hV : ∀ b, (T b).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 : ∀ b, (T b).SizeLE d) (hregular : ∀ b, (T b).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