MovingKernelPairRates.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform prime and integer comparisons for either real giant slice

theorem OAI.Ostmann.PublishedProgressionInput.moving_kernelPair_prime_rate_uniform line 14

Source documentation

The threshold depends on the fixed depth and numerical budget, not the small-prime data, residue class, or other real giant.

theorem PublishedProgressionInput.moving_kernelPair_prime_rate_uniform (P : PublishedProgressionInput)
    (n : ℕ) (C : ℝ) (d : ℕ) :
    ∀ᶠ L : ℝ in atTop, ∀ (σ : Type u) (value : σ → ℕ) (hvalue : ∀ i, value i ≠ 0)
      (childBound pivotBound : ℕ → ℕ) (T : Bool → MovingSlotData σ n) (hf : ∀ b, (T b).Frequencies (· ≠ 0))
      (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi)
      (φ : ℝ → ℝ) (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) (coord : Bool) (fixed : ℝ)
      (Q q a : ℕ), 2 ≤ Q → 1 ≤ q → q ≤ Q → a.Coprime q →
      Real.log (4 * (Q : ℝ)) ≤ 2 * Real.exp ((12 / 1000 : ℝ) * L) →
      ∀ u v : ℝ, Real.exp ((49 / 1000 : ℝ) * L) ≤ u → u ≤ v → v ≤ u + 1 →
      ∀ c : ℂ,
…

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

theorem OAI.Ostmann.PublishedProgressionInput.moving_kernelPair_prime_rate line 79
theorem OAI.Ostmann.moving_kernelPair_integer_bound line 108