CorrectionTails.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Tails of the logarithmic correction moments

Half of the exponential tilt absorbs the logarithmic moment; the other half yields decay in the truncation point.

theorem OAI.JointDickman.log_pow_tail_bound line 16
theorem OAI.JointDickman.correctionLogTerm_tail_bound line 37

theorem OAI.JointDickman.correctionLogMoment_tail_bound line 56

Source documentation

A uniform quantitative error when replacing a truncated correction moment by its convergent full value.

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

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