MovingKernelRates.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform prime and integer comparisons for either real giant slice

def OAI.Ostmann.movingKernelRootBudget line 11

theorem OAI.Ostmann.PublishedProgressionInput.moving_kernel_prime_rate line 16

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_kernel_prime_rate (P : PublishedProgressionInput)
    {σ : Type*} (n : ℕ) (C : ℝ) (d : ℕ) :
    ∀ᶠ L : ℝ in atTop, ∀ (value : σ → ℕ) (hvalue : ∀ i, value i ≠ 0)
      (childBound pivotBound : ℕ → ℕ) (T : MovingSlotData σ n) (hf : T.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.moving_kernel_integer_bound line 68