OAI/NumberTheory/JointDickman/Probability/CorrectionMoments.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The coefficients' actual logarithmic moments

These are absolutely convergent series of the smooth correction. The bounds are uniform in the moving cutoff and every fixed moment order.

  1. def OAI.JointDickman.correctionLogTerm line 17
  2. def OAI.JointDickman.correctionLogMoment line 20
  3. theorem OAI.JointDickman.correctionLogTerm_norm line 23
  4. theorem OAI.JointDickman.correctionLogTerm_summable line 30
  5. theorem OAI.JointDickman.correctionLogMoment_zero line 43
  6. theorem OAI.JointDickman.correctionLogMoment_bound line 51

    Source documentation

    The fixed-order coefficient moments are bounded with one absolute logarithmic exponent.

    theorem correctionLogMoment_bound
    (hM : PublishedInputs.PrimeReciprocalMertensInput) :
    ∃ A : ℝ, 0 < A ∧ ∀ (P : ℕ) (z : ℝ) (k : ℕ),
      2 ≤ P → 1 ≤ Real.log P → 0 ≤ z → z ≤ 1 / 2 →
      |correctionLogMoment (Nat.primesLE P) z k| ≤
        A * (k.factorial : ℝ) * (Real.log P) ^ (Real.exp 1 + k) := by
…

    Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.correctionLogMoment