PositiveLagMass.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual graph has uniformly bounded mass at every positive lag

theorem OAI.JointDickman.graphLagMean_positive_bound line 11

theorem OAI.JointDickman.arithmeticLagMass_positive_bound line 60

Source documentation

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

theorem arithmeticLagMass_positive_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 ≤ auxiliaryCutoff B → ∀ ε : ℝ, 0 < ε →
      ∀ᶠ N : ℕ in atTop, ∀ L : ℕ, ∀ τ C : ℝ,
        arithmeticLagMass B L τ C T N (j : ℤ) ≤
          K*(B : ℝ)*singularFactor 24 j+ε := by
…

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