CoefficientTripleBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform three-form coefficient estimate (manuscript equation (7))

theorem OAI.JointDickman.coefficient_three_form_bound line 16

Source documentation

Rectangles with both side lengths exponential in B have total three-coefficient mass bounded by their area times Σ(j). The estimate is uniform in every positive j and in the position of the rectangle.

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

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