TailSieveParameters.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The actual tail budget at the square-root sieve scale

The auxiliary collision estimate may be applied at Y = X²: its supports are the same fixed infinite-tail residue sets. This choice keeps the endpoint integral when X is integral and covers every prime up to sqrt X.

theorem OAI.Ostmann.tailDefectBudget_doubled_exp line 18
theorem OAI.Ostmann.eventual_sqrt_cutoff_le_tail line 25
theorem OAI.Ostmann.logLogPrimeBand_subset_sqrt_cutoff line 44
theorem OAI.Ostmann.EventuallyPrimeSumset.sqrt_scale_logarithmic_imbalance_with_disjoint line 59
theorem OAI.Ostmann.eventual_affine_square_budget line 86

theorem OAI.Ostmann.EventuallyPrimeSumset.sqrt_scale_sieve_log_budget_with_disjoint line 98

Source documentation

The exact L^(3/4)/16 budget for the multiplier count on the infinite-tail residue supports.

theorem EventuallyPrimeSumset.sqrt_scale_sieve_log_budget_with_disjoint
    (hsize : PublishedSummandSizeBound) {A B : Set ℕ}
    (h : EventuallyPrimeSumset A B) (hA : A.Infinite) (hB : B.Infinite)
    (C : ℝ) (hM : MertensEstimate C) :
    ∃ N : ℕ, (∀ p, p.Prime → Disjoint (tailResidues A N p) (negTailResidues B N p)) ∧
      ∀ᶠ L : ℝ in atTop,
      ∀ X : ℕ, (X : ℝ) = Real.exp (Real.exp L) →
      ∀ P : Finset ℕ, P ⊆ Nat.primesLE ⌊Real.exp (Real.exp L / 2)⌋₊ →
      (∑ p ∈ P, |Real.log
        (((Finset.range p \ tailSupport A N p).card : ℝ) / (tailSupport A N p).card)| / p) ≤
          L ^ (3 / 4 : ℝ) / 16 := by
…

Mentions: OAI.Ostmann.PublishedSummandSizeBound, OAI.Ostmann.EventuallyPrimeSumset, OAI.Ostmann.MertensEstimate, OAI.Ostmann.tailResidues, OAI.Ostmann.negTailResidues, OAI.Ostmann.tailSupport

theorem OAI.Ostmann.EventuallyPrimeSumset.sqrt_scale_logarithmic_imbalance line 120
theorem OAI.Ostmann.EventuallyPrimeSumset.sqrt_scale_sieve_log_budget line 134