TailInitialBroadPriors.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The two actual harmonic priors and their original cutoff centers

theorem OAI.Ostmann.harmonic_prior_prime_bound line 14

theorem OAI.Ostmann.EventuallyPrimeSumset.initial_broad_prior_centers line 27

Source documentation

The bulk center is chosen under its original harmonic prior and balanced event. The spectator center uses the complete retained good-prime pool. Both weights are kept as weights, before selecting any top or compensation cell.

theorem EventuallyPrimeSumset.initial_broad_prior_centers
    (hBonami : PublishedBonamiBound) (P0 : PublishedProgressionInput)
    (H : PublishedRealZeroInput P0) (hSiegel : PublishedSiegelBound)
    (sieve : PublishedQuadraticLargeSieve) (hsize : PublishedSummandSizeBound)
    {C : ℝ} (hM : MertensEstimate C)
    {A B : Set ℕ} (h : EventuallyPrimeSumset A B) (hA : A.Infinite) (hB : B.Infinite)
    (N : ℕ) (hN : ∀ p, p.Prime → Disjoint (tailResidues A N p) (negTailResidues B N p))
    (k cutoff : ℕ) (hk : 2 ≤ k) (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ L : ℝ in atTop, ∀ Y : ℝ,
      Real.exp ((4 / 100 : ℝ) * L) ≤ Y → Y ≤ Real.exp L →
      ∀ hi : ℕ, (hi : ℝ) = Real.exp Y →
      ∀ D : Finset ℕ, (D.card : ℝ) ≤ Real.exp L →
…

Mentions: OAI.Ostmann.PublishedBonamiBound, OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedRealZeroInput, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.PublishedQuadraticLargeSieve, OAI.Ostmann.PublishedSummandSizeBound, OAI.Ostmann.MertensEstimate, OAI.Ostmann.EventuallyPrimeSumset, OAI.Ostmann.tailResidues, OAI.Ostmann.negTailResidues