RoughMomentBounds.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounds for the moving roughness correction

The exponent shift 1 / log P costs only a fixed power of log P. This supplies the moment in Rankin's argument from Mertens' estimate, rather than assuming a cutoff-dependent bound.

theorem OAI.JointDickman.shifted_reciprocal_le line 20
theorem OAI.JointDickman.shifted_prime_sum_le line 31

theorem OAI.JointDickman.smoothCorrection_shifted_bound line 43

Source documentation

Mertens controls the shifted absolute correction moment by a fixed power of the logarithm, uniformly over all finite truncations.

theorem smoothCorrection_shifted_bound
    (hM : PublishedInputs.PrimeReciprocalMertensInput) :
    ∃ A : ℝ, 0 < A ∧ ∀ (P : ℕ) (S : Finset ℕ) (z : ℝ),
      2 ≤ P → 1 ≤ Real.log P → 0 ≤ z → z ≤ 1 / 2 →
      (∑ n ∈ S, |smoothCorrection (Nat.primesLE P) z n| /
        (n : ℝ) ^ (1 - 1 / Real.log P)) ≤
        A * (Real.log P) ^ (Real.exp 1) := by
…

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

theorem OAI.JointDickman.roughConvolutionTail_shifted_bound line 86

Source documentation

The same constant controls the actual large-divisor convolution error.

theorem roughConvolutionTail_shifted_bound
    (hM : PublishedInputs.PrimeReciprocalMertensInput) :
    ∃ A : ℝ, 0 < A ∧ ∀ (P N V : ℕ) (z : ℝ),
      2 ≤ P → 1 ≤ Real.log P → 0 < V → 0 ≤ z → z ≤ 1 / 2 →
      |roughConvolutionTail (Nat.primesLE P) z N V| ≤
        (N : ℝ) / (V : ℝ) ^ (1 / Real.log P) *
          (A * (Real.log P) ^ (Real.exp 1)) := by
…

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

theorem OAI.JointDickman.log_pow_le_rpow line 101

theorem OAI.JointDickman.smoothCorrection_log_moment_le line 116

Source documentation

Exponential tilting controls every logarithmic correction moment.

theorem smoothCorrection_log_moment_le (E S : Finset ℕ) (k : ℕ)
    (z : ℝ) {ε : ℝ} (hε : 0 < ε) :
    (∑ n ∈ S, |smoothCorrection E z n| / (n : ℝ) * (Real.log n) ^ k) ≤
      ((k.factorial : ℝ) / ε ^ k) *
        ∑ n ∈ S, |smoothCorrection E z n| / (n : ℝ) ^ (1 - ε) := by
…

Mentions: OAI.JointDickman.smoothCorrection

theorem OAI.JointDickman.smoothCorrection_log_moments_bound line 138

Source documentation

The absolute constant in the roughness bound works for every fixed moment order; only the factorial and extra logarithmic power change.

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

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