SelbergErrorBound.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Remainder control for the Selberg square sieve

The estimates here retain the actual local remainder. In particular no prime distribution hypothesis is manufactured by passing to square weights.

theorem OAI.Problem337.SelbergError.sum_lambdaSquared_mul line 20

Source documentation

A weighted version of the divisor expansion of the square sieve.

theorem sum_lambdaSquared_mul (P : ℕ) (hP : P ≠ 0)
    (lam f : ℕ → ℝ) :
    (∑ d ∈ P.divisors, BoundingSieve.lambdaSquared lam d * f d) =
      ∑ a ∈ P.divisors, ∑ b ∈ P.divisors,
        lam a * lam b * f (Nat.lcm a b) := by
…

theorem OAI.Problem337.SelbergError.abs_lambdaSquared_le line 57
Source documentation
Absolute square weights are dominated by the square weights of absolute values. This inequality does not assume that the original weights are positive.
```
theorem abs_lambdaSquared_le (lam : ℕ → ℝ) (d : ℕ) :
    |BoundingSieve.lambdaSquared lam d| ≤
      BoundingSieve.lambdaSquared (fun n => |lam n|) d := by
…
```

theorem OAI.Problem337.SelbergError.errSum_lambdaSquared_le line 72

Source documentation

Exact local remainders can be bounded before any uniform estimate is made.

theorem errSum_lambdaSquared_le (s : BoundingSieve) (lam : ℕ → ℝ) :
    s.errSum (BoundingSieve.lambdaSquared lam) ≤
      ∑ a ∈ s.prodPrimes.divisors, ∑ b ∈ s.prodPrimes.divisors,
        |lam a| * |lam b| * |s.rem (Nat.lcm a b)| := by
…

theorem OAI.Problem337.SelbergError.errSum_lambdaSquared_le_sq line 87

Source documentation

A factorizable local remainder envelope gives the usual weighted L1-square bound for the square-sieve error.

theorem errSum_lambdaSquared_le_sq (s : BoundingSieve) (lam w : ℕ → ℝ)
    (hrem : ∀ a ∈ s.prodPrimes.divisors, ∀ b ∈ s.prodPrimes.divisors,
      |s.rem (Nat.lcm a b)| ≤ w a * w b) :
    s.errSum (BoundingSieve.lambdaSquared lam) ≤
      (∑ d ∈ s.prodPrimes.divisors, |lam d| * w d) ^ 2 := by
…