SplitPrimeAfterExclusion.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The split-prime bound after the explicit Page-family deletion

def OAI.Ostmann.splitPrimeMassLower line 12

theorem OAI.Ostmann.split_prime_mass_after_exclusion line 21

Source documentation

The Page condition is discharged using the finite, explicitly constructed exclusion set. No exceptional-character identification is assumed.

theorem split_prime_mass_after_exclusion (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 → 2 < d.natAbs →
        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