OAI/NumberTheory/JointDickman/Counting/GraphCoefficientMass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.graphCoefficientHarmonicTerm line 12
2. theorem OAI.JointDickman.graphCoefficientHarmonicTerm_nonneg line 16
3. theorem OAI.JointDickman.graphCoefficientHarmonic_box line 22
4. theorem OAI.JointDickman.graphCoefficientHarmonic_mass line 79

   Source documentation

   The O(B) dyadic boxes cost only a constant per box after the harmonic denominator is included. This is the coefficient sum in the edge mass.

   theorem graphCoefficientHarmonic_mass
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput) :
       ∃ C : ℝ, 0 < C ∧ ∀ᶠ B : ℕ in atTop,
         ∀ T j : ℕ, 0 < T → (T : ℝ) ≤ Real.exp ((1/10 : ℝ)*B) → j ≠ 0 →
         (∑ bc ∈ amplificationCoefficientPairs B T, graphCoefficientHarmonicTerm B j bc) ≤
           C*(B : ℝ)/(T : ℝ)*singularFactor 24 j := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.amplificationCoefficientPairs, OAI.JointDickman.graphCoefficientHarmonicTerm, OAI.JointDickman.singularFactor