SelbergWeightBound.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.SelbergOptimal.sum_coprime_divisors line 12

Source documentation

Summation over the divisors of a coprime product has no multiplicities.

theorem sum_coprime_divisors {a b : ℕ} (hab : a.Coprime b) (f : ℕ → ℝ) :
    (∑ d ∈ (a * b).divisors, f d) =
      ∑ e ∈ a.divisors, ∑ t ∈ b.divisors, f (e * t) := by
…

theorem OAI.Problem337.SelbergOptimal.coprime_complement line 21
Source documentation
The complementary divisor of a squarefree integer is coprime to it.
```
theorem coprime_complement (s : BoundingSieve) {d : ℕ} (hd : d ∣ s.prodPrimes) :
    d.Coprime (s.prodPrimes / d) := by
…
```

theorem OAI.Problem337.SelbergOptimal.normalizer_decompose line 27

Source documentation

Split the finite Selberg normalizer at a divisor of the sieving product.

theorem normalizer_decompose (s : BoundingSieve) (z : ℕ) {d : ℕ}
    (hd : d ∣ s.prodPrimes) :
    normalizer s z =
      ∑ e ∈ d.divisors, ∑ t ∈ (s.prodPrimes / d).divisors,
        if e * t ≤ z then s.selbergTerms e * s.selbergTerms t else 0 := by
…

Mentions: OAI.Problem337.SelbergOptimal.normalizer

theorem OAI.Problem337.SelbergOptimal.sum_selbergTerms_divisors line 44
theorem OAI.Problem337.SelbergOptimal.truncated_complement_sum_le_normalizer line 53
Source documentation
The positive numerator of an optimal Selberg weight is a subsum of the normalizer, after splitting into complementary divisor coordinates.
```
theorem truncated_complement_sum_le_normalizer (s : BoundingSieve) (z : ℕ)
    {d : ℕ} (hd : d ∣ s.prodPrimes) :
    (s.selbergTerms d / s.nu d) *
        (∑ t ∈ (s.prodPrimes / d).divisors,
          if d * t ≤ z then s.selbergTerms t else 0) ≤ normalizer s z := by
…
```
Mentions: OAI.Problem337.SelbergOptimal.normalizer

theorem OAI.Problem337.SelbergOptimal.truncated_div_sum_le_normalizer line 79

Source documentation

The same bound in the quotient-cutoff form used in the explicit weights.

theorem truncated_div_sum_le_normalizer (s : BoundingSieve) (z : ℕ)
    {d : ℕ} (hd : d ∣ s.prodPrimes) :
    (s.selbergTerms d / s.nu d) *
        (∑ t ∈ (s.prodPrimes / d).divisors,
          if t ≤ z / d then s.selbergTerms t else 0) ≤ normalizer s z := by
…

Mentions: OAI.Problem337.SelbergOptimal.normalizer

theorem OAI.Problem337.SelbergOptimal.abs_normalized_complement_le_one line 91

Source documentation

The normalized explicit optimal-weight expression has absolute value at most one. This bound is independent of the local sieve dimension.

theorem abs_normalized_complement_le_one (s : BoundingSieve) {z : ℕ}
    (hz : 1 ≤ z) {d : ℕ} (hd : d ∣ s.prodPrimes) :
    |(μ d : ℝ) * (s.selbergTerms d / s.nu d) /
        normalizer s z *
        (∑ t ∈ (s.prodPrimes / d).divisors,
          if t ≤ z / d then s.selbergTerms t else 0)| ≤ 1 := by
…

Mentions: OAI.Problem337.SelbergOptimal.normalizer