GridMultiplicityBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

One tolerance and vanishing errors for every grid cell

theorem OAI.JointDickman.finite_positive_bound line 12

theorem OAI.JointDickman.exists_grid_multiplicity_bounds line 26

Source documentation

The actual sieve estimates at both endpoints hold for the same positive tolerance, with a nonnegative vanishing majorant on every later grid cell.

theorem exists_grid_multiplicity_bounds
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput)
    {L : ℕ} (hL : 10000 ≤ L) {η cap : ℝ} (hη : 0 < η) (hcap : 0 < cap) :
    ∃ τ : ℝ, 0 < τ ∧ τ ≤ cap ∧ τ ≤ samplingTau ∧
      smallMultiplicityExponent L τ < 8/1000 ∧
      ∃ E : ℕ → ℕ → ℝ, (∀ k B, 0 ≤ E k B) ∧
        (∀ k ∈ Icc 4 L, Tendsto (E k) atTop (𝓝 0)) ∧
        ∀ᶠ B : ℕ in atTop, ∀ k ∈ Icc 4 L,
          ∀ (C : ℝ) (A D V : Finset ℕ) (j : ℕ),
            A ⊆ auxiliaryPrimes B → D ⊆ auxiliaryPrimes B → V ⊆ auxiliaryPrimes B →
            RegularPrimeSet B L τ C A → RegularPrimeSet B L τ C D → RegularPrimeSet B L τ C V →
…

Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.samplingTau, OAI.JointDickman.smallMultiplicityExponent, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.RegularPrimeSet