OAI/NumberTheory/JointDickman/Arithmetic/NumericSieveError.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Negligibility of the large-addition sieve remainder

  1. theorem OAI.JointDickman.numeric_sieve_scaled_error_tendsto line 13

    Source documentation

    At separated powers, the explicit polynomial sieve remainder is smaller than every fixed power of B, uniformly in the allowed lag.

    theorem numeric_sieve_scaled_error_tendsto {g a : ℝ} (ha : 0 < a) (hga : g < a) (D : ℝ) :
    Tendsto (fun B : ℝ => 32*B^(D+2)*Real.exp (3*B^g-B^a)) atTop (𝓝 0) := by
…
  2. theorem OAI.JointDickman.numeric_sieve_remainder_small line 36