OAI/NumberTheory/JointDickman/Counting/SignedCoefficientSums.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.coefficientRelationWeight line 14
2. def OAI.JointDickman.signedCoefficientMass line 18
3. theorem OAI.JointDickman.coefficientRelationWeight_neg line 21
4. theorem OAI.JointDickman.signedCoefficientMass_neg line 28
5. theorem OAI.JointDickman.coefficientRelationWeight_nat line 34
6. theorem OAI.JointDickman.signedCoefficientMass_nat_le line 47
7. theorem OAI.JointDickman.signed_coefficient_three_form_bound line 66

   Source documentation

   Both signs of the lag satisfy the same rectangle bound, including the support restriction that both a and b belong to the coefficient interval.

   theorem signed_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 →
         signedCoefficientMass B j (Ico u v) (Ico w x) ≤
           C * ((v : ℝ) - u) * ((x : ℝ) - w) * singularFactor 24 j.natAbs := by
   …

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