CandidateMultiplicityBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform expected multiplicity of actual coefficient representations

theorem OAI.JointDickman.tiltedCandidatePairCount_bound line 15

Source documentation

The entire representation count, including both large-addition orientations, is at most twice the small-addition power under the two first-representation remainder laws. Only Ford's sieve and Mertens enter.

theorem tiltedCandidatePairCount_bound
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput)
    {L : ℕ} (hL : 10000 ≤ L) {η cap : ℝ} (hη : 0 < η) (hcap : 0 < cap) :
    ∃ τ : ℝ, 0 < τ ∧ τ ≤ cap ∧ τ ≤ samplingTau ∧
      ∀ᶠ B : ℕ in atTop, ∀ (T H M : ℕ) (C : ℝ) (i t : Fin M) (A D : Finset ℕ),
        (T : ℝ) ≤ Real.exp B →
        A ⊆ auxiliaryPrimes B → D ⊆ auxiliaryPrimes B →
        RegularPrimeSet B L τ C A → RegularPrimeSet B L τ C D →
        (∏ p ∈ A, p : ℕ) ≤ Real.exp ((16/5 : ℝ)*B) →
        (∏ p ∈ D, p : ℕ) ≤ Real.exp ((16/5 : ℝ)*B) →
        0 < t.val-i.val → t.val-i.val ≤ auxiliaryCutoff B →
…

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