SignedLagMass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Both signs of the actual lag-mass bound

theorem OAI.JointDickman.graphTriple_harmonic_signed_bound line 11
theorem OAI.JointDickman.graphLagMean_signed_bound line 33

theorem OAI.JointDickman.arithmeticLagMass_signed_bound line 82

Source documentation

All regularity parameters are bounded simultaneously. They enter only the nonnegative weights already dominated by the same majorant.

theorem arithmeticLagMass_signed_bound
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) :
    ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop, ∀ T : ℕ, ∀ j : ℤ,
      0 < T → (T : ℝ) ≤ Real.exp ((1/10 : ℝ)*B) → j ≠ 0 →
      j.natAbs ≤ auxiliaryCutoff B → ∀ ε : ℝ, 0 < ε →
      ∀ᶠ N : ℕ in atTop, ∀ L : ℕ, ∀ τ C : ℝ,
        arithmeticLagMass B L τ C T N j ≤
          K*(B : ℝ)*singularFactor 24 j.natAbs+ε := by
…

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