AllKernelSplitMass.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The retained split-prime estimate for every nonzero squarefree kernel

theorem OAI.Ostmann.all_kernel_split_prime_mass line 14

Source documentation

This includes the principal kernel 1 and all three small nonprincipal kernels. The constants and exclusion set are uniform over every kernel.

theorem all_kernel_split_prime_mass (P : PublishedProgressionInput)
    (H : PublishedRealZeroInput P) (hSiegel : PublishedSiegelBound)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ A K C : ℝ, 0 < A ∧ 0 < K ∧ 0 < C ∧
      ∀ (d : ℤ) (Q₀ Q D Y : ℕ) (R s : ℝ),
        Squarefree d.natAbs → d ≠ 0 →
        2 ≤ Q₀ → 4 * d.natAbs ≤ Q₀ → 0 < Q → 0 < D → 0 < Y →
        d.natAbs ∣ D → 0 ≤ R →
        2 * (A + H.errorConstant) ≤ Real.log (4 * (Q₀ : ℝ)) →
        1 < s → s ≤ 2 → s ≤ 1 + 1 / Real.log (4 * (Q₀ : ℝ)) →
        d ∉ pageKernelExclusion P Q₀ R →
        splitPrimeMassLower P H A K C ε Q₀ Q D Y R s ≤
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedRealZeroInput, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.pageKernelExclusion, OAI.Ostmann.splitPrimeMassLower