KernelCountFromCenter.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The quadratic sieve counts the kernels of the actual common-center bias

theorem OAI.Ostmann.quadratic_count_scalar_budget line 12
theorem OAI.Ostmann.eventual_kernel_count_prefactor line 23

theorem OAI.Ostmann.eventual_kernel_count_from_commonCenter line 51

Source documentation

A concrete version of the manuscript's X^(3 epsilon + o(1)) count. The common-center loss and distinct-tuple error are both discharged.

theorem eventual_kernel_count_from_commonCenter (sieve : PublishedQuadraticLargeSieve)
    (Cpop : ℝ) (hCpop : 500 ≤ Cpop)
    (ε c : ℝ) (hε : 0 < ε) (hc : 0 < c) :
    ∀ᶠ T : ℝ in atTop, ∀ (L J : ℝ) (P : Finset ℕ) (r Z M : ℕ)
      (e : ℕ → ℂ) (U : Finset ℤ),
      T ^ (3 / 2 : ℝ) ≤ L → 2 ≤ r → (r : ℝ) ≤ 2 * T ^ (3 / 5 : ℝ) →
      0 < J → Real.exp T ≤ Cpop * T * J →
      J * Real.exp (-T / (r - 1 : ℕ)) ≤ P.card →
      Real.exp (3 * T / 5) ≤ P.card → (Z : ℝ) ≤ Real.exp (T + 1) →
      1 ≤ Z → 1 ≤ M → M ≤ Z ^ r → ((Z : ℝ) ^ r) ≤ Real.exp (2 * L) →
      (∀ p ∈ P, p.Prime) → (∀ p ∈ P, Odd p) → (∀ p ∈ P, p ≤ Z) →
      (∀ p ∈ P, ‖e p‖ ≤ 1) → U ⊆ signedSquarefreeRange M →
…

Mentions: OAI.Ostmann.PublishedQuadraticLargeSieve, OAI.Ostmann.signedSquarefreeRange