SelbergOptimal.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.SelbergOptimal.sum_multiples_complement line 13

Source documentation

Complementation turns a sum over multiples among divisors into a divisor sum.

theorem sum_multiples_complement (P l : ℕ) (hP : P ≠ 0) (hl : l ∣ P)
    (f : ℕ → ℝ) :
    (∑ d ∈ P.divisors, if l ∣ d then f (P / d) else 0) =
      ∑ d ∈ (P / l).divisors, f d := by
…

def OAI.Problem337.SelbergOptimal.upperInverse line 44
Source documentation
Inverse of the upper divisor-sum transform, expressed through ordinary Möbius inversion after complementing divisors.
```
def upperInverse (P : ℕ) (y : ℕ → ℝ) (d : ℕ) : ℝ :=
…
```
theorem OAI.Problem337.SelbergOptimal.sum_upperInverse line 47
theorem OAI.Problem337.SelbergOptimal.upperInverse_one line 62
def OAI.Problem337.SelbergOptimal.normalizer line 71
Source documentation
The positive finite normalizing sum of the optimal Selberg weights.
```
def normalizer (s : BoundingSieve) (z : ℕ) : ℝ :=
…
```
theorem OAI.Problem337.SelbergOptimal.normalizer_pos line 74
def OAI.Problem337.SelbergOptimal.optimalDiagonal line 86
Source documentation
The diagonal coordinates attaining the constrained minimum.
```
def optimalDiagonal (s : BoundingSieve) (z d : ℕ) : ℝ :=
…
```
def OAI.Problem337.SelbergOptimal.optimalWeight line 90
Source documentation
Selberg weights obtained by upper Möbius inversion.
```
def optimalWeight (s : BoundingSieve) (z d : ℕ) : ℝ :=
…
```
theorem OAI.Problem337.SelbergOptimal.optimalWeight_transform line 94
theorem OAI.Problem337.SelbergOptimal.optimalWeight_one line 111
theorem OAI.Problem337.SelbergOptimal.mainSum_optimalWeight line 133
Source documentation
The diagonalized main term at the optimal weights is exactly the reciprocal of the finite Selberg normalizer.
```
theorem mainSum_optimalWeight (s : BoundingSieve) {z : ℕ} (hz : 1 ≤ z) :
    s.mainSum (BoundingSieve.lambdaSquared (optimalWeight s z)) =
      1 / normalizer s z := by
…
```
Mentions: OAI.Problem337.SelbergOptimal.optimalWeight, OAI.Problem337.SelbergOptimal.normalizer
theorem OAI.Problem337.SelbergOptimal.siftedSum_le line 160
Source documentation
The Selberg upper-bound sieve with its main term optimized.
```
theorem siftedSum_le (s : BoundingSieve) {z : ℕ} (hz : 1 ≤ z) :
    s.siftedSum ≤ s.totalMass / normalizer s z +
      s.errSum (BoundingSieve.lambdaSquared (optimalWeight s z)) := by
…
```
Mentions: OAI.Problem337.SelbergOptimal.normalizer, OAI.Problem337.SelbergOptimal.optimalWeight
theorem OAI.Problem337.SelbergOptimal.optimalWeight_eq_zero_of_lt line 170
Source documentation
No optimal weight lies above the chosen truncation.
```
theorem optimalWeight_eq_zero_of_lt (s : BoundingSieve) {z d : ℕ} (hzd : z < d) :
    optimalWeight s z d = 0 := by
…
```
Mentions: OAI.Problem337.SelbergOptimal.optimalWeight
theorem OAI.Problem337.SelbergOptimal.abs_upperInverse_le line 194
Source documentation
Upper Möbius inversion does not increase the crude full-divisor absolute-mass bound. This estimate is independent of squarefreeness.
```
theorem abs_upperInverse_le (P d : ℕ) (hP : P ≠ 0) (hd : d ∣ P)
    (y : ℕ → ℝ) :
    |upperInverse P y d| ≤ ∑ e ∈ P.divisors, |y e| := by
…
```
Mentions: OAI.Problem337.SelbergOptimal.upperInverse
theorem OAI.Problem337.SelbergOptimal.sum_abs_optimalDiagonal line 219
Source documentation
The optimal diagonal coordinates have total absolute mass one.
```
theorem sum_abs_optimalDiagonal (s : BoundingSieve) {z : ℕ} (hz : 1 ≤ z) :
    (∑ d ∈ s.prodPrimes.divisors, |optimalDiagonal s z d|) = 1 := by
…
```
Mentions: OAI.Problem337.SelbergOptimal.optimalDiagonal
theorem OAI.Problem337.SelbergOptimal.abs_optimalWeight_le line 239
Source documentation
A coefficient bound adequate for polynomial-error applications of the sieve.
```
theorem abs_optimalWeight_le (s : BoundingSieve) {z d : ℕ} (hz : 1 ≤ z)
    (hd : d ∣ s.prodPrimes) :
    |optimalWeight s z d| ≤ (s.nu d)⁻¹ := by
…
```
Mentions: OAI.Problem337.SelbergOptimal.optimalWeight

theorem OAI.Problem337.SelbergOptimal.upperInverse_eq_sum_multiples line 250

Source documentation

The upper inverse in the more usual sum-over-multiples form.

theorem upperInverse_eq_sum_multiples (P d : ℕ) (hP : P ≠ 0) (hd : d ∣ P)
    (y : ℕ → ℝ) :
    upperInverse P y d =
      ∑ e ∈ P.divisors, if d ∣ e then (μ (e / d) : ℝ) * y e else 0 := by
…

Mentions: OAI.Problem337.SelbergOptimal.upperInverse

theorem OAI.Problem337.SelbergOptimal.sum_multiples_eq line 272

Source documentation

Divisor multiples are parametrized by the complementary quotient.

theorem sum_multiples_eq (P d : ℕ) (hP : P ≠ 0) (hd : d ∣ P)
    (f : ℕ → ℝ) :
    (∑ e ∈ P.divisors, if d ∣ e then f e else 0) =
      ∑ t ∈ (P / d).divisors, f (d * t) := by
…

theorem OAI.Problem337.SelbergOptimal.moebius_div_mul line 303
Source documentation
The two Möbius signs from upper inversion collapse on squarefree divisors.
```
theorem moebius_div_mul (e d : ℕ) (he : Squarefree e) (hd : d ∣ e) :
    (μ (e / d) : ℝ) * (μ e : ℝ) = (μ d : ℝ) := by
…
```
def OAI.Problem337.SelbergOptimal.complementNormalizer line 319
Source documentation
The truncated normalizer on complementary divisors.
```
def complementNormalizer (s : BoundingSieve) (z d : ℕ) : ℝ :=
…
```
theorem OAI.Problem337.SelbergOptimal.optimalWeight_formula line 324
Source documentation
Explicit classical formula for the optimal coefficient. In particular, the sign is the Möbius sign and the remaining factors are nonnegative.
```
theorem optimalWeight_formula (s : BoundingSieve) (z d : ℕ)
    (hd : d ∣ s.prodPrimes) :
    optimalWeight s z d = (μ d : ℝ) * s.selbergTerms d / s.nu d *
      (complementNormalizer s z d / normalizer s z) := by
…
```
Mentions: OAI.Problem337.SelbergOptimal.optimalWeight, OAI.Problem337.SelbergOptimal.complementNormalizer, OAI.Problem337.SelbergOptimal.normalizer