TailSpectatorSupply.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Spectator primes for the actual normalized tail transforms

theorem OAI.Ostmann.eventual_tail_spectator_supply line 11

theorem OAI.Ostmann.EventuallyPrimeSumset.tail_spectator_supply line 89

Source documentation

The spectator supply at any fixed admissible tail cutoff, with all character smallness derived from the cited published inputs.

theorem EventuallyPrimeSumset.tail_spectator_supply
    (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))
    (α β ε c : ℝ) (hα : 0 < α) (hαβ : α < β) (hε : 0 < ε) (hc : 0 < c) :
    ∀ᶠ L : ℝ in atTop, ∀ P : Finset ℕ, P ⊆ closedLogLogPrimeBand α β L →
      ∃ Q ⊆ P, (∑ p ∈ P, (p : ℝ)⁻¹) - c * L ≤ ∑ p ∈ Q, (p : ℝ)⁻¹ ∧
        ∀ p ∈ Q, 3 ≤ p ∧
          (1 / 3 : ℝ) ≤ residueDensity (tailDensityMask A N p) ∧
…

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, OAI.Ostmann.closedLogLogPrimeBand, OAI.Ostmann.residueDensity, OAI.Ostmann.tailDensityMask