SmoothRankinBounds.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.uniform_divisor_smooth_rankin_bound line 13

Source documentation

Uniform Rankin estimate for smooth harmonic divisor moments. The constant depends only on the moment order, not on the smoothness cutoff or the tail.

theorem uniform_divisor_smooth_rankin_bound (r : ℕ) :
    ∃ C : ℝ, 0 < C ∧ ∀ β V : ℝ, 0 ≤ β → β ≤ 1 / 4 →
      ∀ N : ℕ, ∀ s : Finset ℕ,
      (∀ n ∈ s, n ∈ N.smoothNumbers) →
      (∀ n ∈ s, Real.exp V ≤ (n : ℝ)) →
      (∑ n ∈ s, (n.divisors.card : ℝ) ^ r / (n : ℝ)) ≤
        Real.exp (-β * V + C * ∑ p ∈ N.primesBelow, (p : ℝ) ^ (β - 1)) := by
…

theorem OAI.Problem337.prime_rpow_sum_le_exp_mul_reciprocals line 33

Source documentation

Prime powers with exponent just above -1 are estimated by prime reciprocals, with the customary exponential loss at the smoothness scale.

theorem prime_rpow_sum_le_exp_mul_reciprocals {β W : ℝ} (hβ : 0 ≤ β)
    (N : ℕ) (hN : (N : ℝ) ≤ Real.exp W) :
    (∑ p ∈ N.primesBelow, (p : ℝ) ^ (β - 1)) ≤
      Real.exp (β * W) * ∑ p ∈ N.primesBelow, (1 : ℝ) / (p : ℝ) := by
…

theorem OAI.Problem337.uniform_divisor_smooth_rankin_reciprocal_bound line 51

Source documentation

The smooth-prefix estimate in the form used for intermediate-prime bands. All remaining number theory is isolated in the prime reciprocal sum, rather than in a product over local factors.

theorem uniform_divisor_smooth_rankin_reciprocal_bound (r : ℕ) :
    ∃ C : ℝ, 0 < C ∧ ∀ β V W : ℝ, 0 ≤ β → β ≤ 1 / 4 →
      ∀ N : ℕ, (N : ℝ) ≤ Real.exp W → ∀ s : Finset ℕ,
      (∀ n ∈ s, n ∈ N.smoothNumbers) →
      (∀ n ∈ s, Real.exp V ≤ (n : ℝ)) →
      (∑ n ∈ s, (n.divisors.card : ℝ) ^ r / (n : ℝ)) ≤
        Real.exp (-β * V + C * Real.exp (β * W) *
          ∑ p ∈ N.primesBelow, (1 : ℝ) / (p : ℝ)) := by
…

theorem OAI.Problem337.rankin_band_negative_exponent line 66
theorem OAI.Problem337.rankin_band_positive_exponent line 72
theorem OAI.Problem337.log_one_add_two_mul_le line 80