FiniteEulerBound.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.DivisorMoment.sum_Icc_le_factorial_euler line 10

Source documentation

A nonnegative multiplicative function is bounded by its finite Euler product.

theorem sum_Icc_le_factorial_euler (f : ArithmeticFunction ℝ)
    (hf : f.IsMultiplicative) (hpos : ∀ n, 0 ≤ f n) (T : ℕ) :
    (∑ n ∈ Finset.Icc 1 T, f n) ≤
      ∏ p ∈ T.factorial.primeFactors,
        ∑ j ∈ Finset.range (T.factorial.factorization p + 1), f (p ^ j) := by
…

theorem OAI.Problem337.DivisorMoment.sum_Icc_le_exp_prime_sum line 38

Source documentation

An exponential local bound turns the finite Euler product into a prime sum.

theorem sum_Icc_le_exp_prime_sum (f : ArithmeticFunction ℝ)
    (hf : f.IsMultiplicative) (hpos : ∀ n, 0 ≤ f n)
    (T : ℕ) (C : ℝ) (w : ℕ → ℝ)
    (hlocal : ∀ p, p.Prime → p ≤ T → ∀ L : ℕ,
      (∑ j ∈ Finset.range (L + 1), f (p ^ j)) ≤ Real.exp (C * w p)) :
    (∑ n ∈ Finset.Icc 1 T, f n) ≤
      Real.exp (C * ∑ p ∈ T.factorial.primeFactors, w p) := by
…

def OAI.Problem337.DivisorMoment.divisorMomentWeight line 55
Source documentation
The multiplicative weight used in harmonic and Rankin divisor moments.
```
def divisorMomentWeight (r : ℕ) (σ : ℝ) : ArithmeticFunction ℝ :=
…
```
theorem OAI.Problem337.DivisorMoment.divisorMomentWeight_nonneg line 58
theorem OAI.Problem337.DivisorMoment.divisorMomentWeight_multiplicative line 66
theorem OAI.Problem337.DivisorMoment.divisorMomentWeight_prime_pow line 77

theorem OAI.Problem337.DivisorMoment.divisor_moment_sum_le_euler line 89

Source documentation

Divisor moments bounded by a truncated prime-power Euler product.

theorem divisor_moment_sum_le_euler (r T : ℕ) (σ : ℝ) :
    (∑ n ∈ Finset.Icc 1 T, (n.divisors.card : ℝ) ^ r * (n : ℝ) ^ (-σ)) ≤
      ∏ p ∈ T.factorial.primeFactors,
        ∑ j ∈ Finset.range (T.factorial.factorization p + 1),
          (j + 1 : ℝ) ^ r * ((p : ℝ) ^ (-σ)) ^ j := by
…

def OAI.Problem337.DivisorMoment.smoothRestriction line 108
Source documentation
Restriction to integers supported on a prescribed finite prime set.
```
def smoothRestriction (P : Finset ℕ) (f : ArithmeticFunction ℝ) : ArithmeticFunction ℝ :=
…
```
theorem OAI.Problem337.DivisorMoment.smoothRestriction_multiplicative line 111
theorem OAI.Problem337.DivisorMoment.smoothRestriction_nonneg line 121
theorem OAI.Problem337.DivisorMoment.smoothRestriction_local line 128

theorem OAI.Problem337.DivisorMoment.sum_smooth_le_factorial_euler line 140

Source documentation

The same Euler bound restricted to smooth integers uses only their allowed primes.

theorem sum_smooth_le_factorial_euler (P : Finset ℕ) (f : ArithmeticFunction ℝ)
    (hf : f.IsMultiplicative) (hpos : ∀ n, 0 ≤ f n) (T : ℕ) :
    (∑ n ∈ (Finset.Icc 1 T).filter (fun n => n.primeFactors ⊆ P), f n) ≤
      ∏ p ∈ T.factorial.primeFactors ∩ P,
        ∑ j ∈ Finset.range (T.factorial.factorization p + 1), f (p ^ j) := by
…

theorem OAI.Problem337.DivisorMoment.sum_smooth_le_exp_prime_sum line 155

Source documentation

Exponential version of the smooth Euler bound.

theorem sum_smooth_le_exp_prime_sum (P : Finset ℕ) (f : ArithmeticFunction ℝ)
    (hf : f.IsMultiplicative) (hpos : ∀ n, 0 ≤ f n)
    (T : ℕ) (C : ℝ) (w : ℕ → ℝ)
    (hlocal : ∀ p, p.Prime → p ≤ T → p ∈ P → ∀ L : ℕ,
      (∑ j ∈ Finset.range (L + 1), f (p ^ j)) ≤ Real.exp (C * w p)) :
    (∑ n ∈ (Finset.Icc 1 T).filter (fun n => n.primeFactors ⊆ P), f n) ≤
      Real.exp (C * ∑ p ∈ T.factorial.primeFactors ∩ P, w p) := by
…

theorem OAI.Problem337.DivisorMoment.local_divisor_sum_pos line 172

theorem OAI.Problem337.DivisorMoment.divisor_moment_sum_le_exp line 181

Source documentation

A uniform logarithmic local-factor bound controls the harmonic divisor sum.

theorem divisor_moment_sum_le_exp (r T : ℕ) (σ C : ℝ)
    (hlocal : ∀ p, p.Prime → p ≤ T → ∀ L : ℕ,
      Real.log (∑ j ∈ Finset.range (L + 1),
        (j + 1 : ℝ) ^ r * ((p : ℝ) ^ (-σ)) ^ j) ≤ C * (p : ℝ) ^ (-σ)) :
    (∑ n ∈ Finset.Icc 1 T, (n.divisors.card : ℝ) ^ r * (n : ℝ) ^ (-σ)) ≤
      Real.exp (C * ∑ p ∈ T.factorial.primeFactors, (p : ℝ) ^ (-σ)) := by
…

theorem OAI.Problem337.DivisorMoment.smooth_divisor_moment_sum_le_exp line 203

Source documentation

Smooth analogue, used after the Rankin weight is inserted.

theorem smooth_divisor_moment_sum_le_exp (P : Finset ℕ) (r T : ℕ) (σ C : ℝ)
    (hlocal : ∀ p, p.Prime → p ≤ T → p ∈ P → ∀ L : ℕ,
      Real.log (∑ j ∈ Finset.range (L + 1),
        (j + 1 : ℝ) ^ r * ((p : ℝ) ^ (-σ)) ^ j) ≤ C * (p : ℝ) ^ (-σ)) :
    (∑ n ∈ (Finset.Icc 1 T).filter (fun n => n.primeFactors ⊆ P),
      (n.divisors.card : ℝ) ^ r * (n : ℝ) ^ (-σ)) ≤
      Real.exp (C * ∑ p ∈ T.factorial.primeFactors ∩ P, (p : ℝ) ^ (-σ)) := by
…