OAI/NumberTheory/Ostmann/Arithmetic/BulkLogSliceComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.bulkSmoothComparisonBudget line 13
2. def OAI.Ostmann.bulkPrimeErrorFactor line 18
3. theorem OAI.Ostmann.PublishedProgressionInput.bulk_log_slice_comparison line 24

   Source documentation

   An actual one-coordinate comparison, uniformly in the remaining real bulk logarithms. The finite prime measure includes both boundary conventions exactly.

   theorem PublishedProgressionInput.bulk_log_slice_comparison
       (P : PublishedProgressionInput) {σ : Type*} [Fintype σ]
       (base : σ → ℝ) (S : Finset σ) {n : ℕ} (T : MovingSlotData σ n)
       (i : σ) (hiS : i ∈ S) (hT : T.CompensationAbsent i)
       (ψ : 𝓢(ℝ, ℂ)) (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 : ℕ) (hsize : T.SizeLE d) (hregular : T.RegularLengthLE r)
       (L R : ℝ) (f : (σ → ℝ) →ᵇ ℂ)
       (hf : ∀ x, f x = realValueSmoothWeight (bulkLogValues base S x) T ψ X lo hi hlo hhi φ G L R)
   …

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