DivisorTupleBounds.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Elementary summatory bounds for divisor tuples

These finite hyperbola estimates supply logarithmic remainder bounds for square sieves. They do not use a prime number theorem.

def OAI.Problem337.SelbergError.divisorTupleCount line 17
Source documentation
Ordered positive factor tuples, expressed by Dirichlet powers of zeta.
```
def divisorTupleCount (k n : ℕ) : ℕ :=
…
```
lemma OAI.Problem337.SelbergError.sum_divisorsAntidiagonal_le_rectangle line 20

theorem OAI.Problem337.SelbergError.harmonic_convolution_le line 56

Source documentation

The harmonic norm on an initial interval is submultiplicative for Dirichlet convolution of nonnegative arithmetic functions.

theorem harmonic_convolution_le (f g : ArithmeticFunction ℕ) (N : ℕ) :
    (∑ n ∈ Icc 1 N, ((f * g) n : ℝ) / n) ≤
      (∑ a ∈ Icc 1 N, (f a : ℝ) / a) *
      (∑ b ∈ Icc 1 N, (g b : ℝ) / b) := by
…

lemma OAI.Problem337.SelbergError.zeta_harmonic_sum line 76
theorem OAI.Problem337.SelbergError.divisorTuple_harmonic_le line 87
Source documentation
The harmonic sum over ordered k-factor tuples has at most the expected k logarithmic factors.
```
theorem divisorTuple_harmonic_le (k N : ℕ) :
    (∑ n ∈ Icc 1 N, (divisorTupleCount k n : ℝ) / n) ≤
      (harmonic N : ℝ) ^ k := by
…
```
Mentions: OAI.Problem337.SelbergError.divisorTupleCount
theorem OAI.Problem337.SelbergError.divisorTuple_sum_le line 111
Source documentation
A uniform summatory bound, with one harmless extra logarithmic factor. It holds also at N = 0 and requires no squarefreeness restriction.
```
theorem divisorTuple_sum_le (k N : ℕ) :
    (∑ n ∈ Icc 1 N, (divisorTupleCount k n : ℝ)) ≤
      (N : ℝ) * (harmonic N : ℝ) ^ k := by
…
```
Mentions: OAI.Problem337.SelbergError.divisorTupleCount
theorem OAI.Problem337.SelbergError.divisorTupleCount_prime line 127
Source documentation
At a prime, there are exactly k ordered k-factor tuples.
```
theorem divisorTupleCount_prime (k p : ℕ) (hp : p.Prime) :
    divisorTupleCount k p = k := by
…
```
Mentions: OAI.Problem337.SelbergError.divisorTupleCount
theorem OAI.Problem337.SelbergError.divisorTupleCount_squarefree line 141
Source documentation
A squarefree number has one independent choice among k tuple positions for every prime factor.
```
theorem divisorTupleCount_squarefree (k n : ℕ) (hn : Squarefree n) :
    divisorTupleCount k n = k ^ n.primeFactors.card := by
…
```
Mentions: OAI.Problem337.SelbergError.divisorTupleCount
theorem OAI.Problem337.SelbergError.divisorTuple_sum_le_log line 155
Source documentation
Explicit elementary logarithmic summatory majorant.
```
theorem divisorTuple_sum_le_log (k N : ℕ) :
    (∑ n ∈ Icc 1 N, (divisorTupleCount k n : ℝ)) ≤
      (N : ℝ) * (1 + Real.log N) ^ k := by
…
```
Mentions: OAI.Problem337.SelbergError.divisorTupleCount

theorem OAI.Problem337.SelbergError.sum_squarefree_pow_le line 165

Source documentation

A finite squarefree support has a power-of-prime-count sum bounded by an elementary divisor-tuple sum.

theorem sum_squarefree_pow_le (S : Finset ℕ) (k N : ℕ)
    (hS : ∀ n ∈ S, Squarefree n) (hSN : S ⊆ Icc 1 N) :
    (∑ n ∈ S, (k : ℝ) ^ n.primeFactors.card) ≤
      (N : ℝ) * (1 + Real.log N) ^ k := by
…