CoefficientPairBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform fixed-coefficient two-form estimate (equation (6))

theorem OAI.JointDickman.coefficient_two_form_bound line 15

Source documentation

The fixed rough coefficient contributes only a bounded Euler factor; all dependence on the nonzero positive slope is through the singular factor.

theorem coefficient_two_form_bound
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput)
    {δ : ℝ} (hδ : 0 < δ) (κ : ℝ) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ B : ℕ in atTop, ∀ j b u v : ℕ,
      j ≠ 0 → b ≠ 0 → (b : ℝ) ≤ Real.exp (κ * B) →
      Disjoint b.primeFactors (Nat.primesLE (auxiliaryCutoff B)) →
      u ≤ v → Real.exp (δ * B) ≤ (v : ℝ) - u →
      (∑ n ∈ Ico u v, coefficientWeight B n * coefficientWeight B (b + j * n)) ≤
        C * ((v : ℝ) - u) * singularFactor 24 j := by
…

Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.coefficientWeight, OAI.JointDickman.singularFactor