SmoothRankin.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.smooth_sum_le_euler_product line 12

Source documentation

A finite nonnegative sum over smooth numbers is bounded by the finite Euler product. Only the local prime-power series need to be summable.

theorem smooth_sum_le_euler_product
    (f : ℕ → ℝ) (hf : ∀ n, 0 ≤ f n) (hf1 : f 1 = 1)
    (hmul : ∀ {m n}, Nat.Coprime m n → f (m * n) = f m * f n)
    (hsum : ∀ {p : ℕ}, p.Prime → Summable (fun j : ℕ => ‖f (p ^ j)‖))
    (N : ℕ) (s : Finset ℕ) (hs : ∀ n ∈ s, n ∈ N.smoothNumbers) :
    (∑ n ∈ s, f n) ≤ ∏ p ∈ N.primesBelow, ∑' j : ℕ, f (p ^ j) := by
…

theorem OAI.Problem337.rankin_weight_bound line 29

Source documentation

The elementary exponential weight used in Rankin's tail estimate.

theorem rankin_weight_bound {V β : ℝ} {n : ℕ}
    (hβ : 0 ≤ β) (hn : Real.exp V ≤ (n : ℝ)) :
    1 ≤ Real.exp (-β * V) * (n : ℝ) ^ β := by
…

theorem OAI.Problem337.smooth_rankin_bound line 43

Source documentation

Rankin's trick followed by a finite Euler product. This form applies to f n = τ(n)^r / n; the local weight then has exponent -1 + β.

theorem smooth_rankin_bound
    (f : ℕ → ℝ) (hf : ∀ n, 0 ≤ f n) (hf1 : f 1 = 1)
    (hmul : ∀ {m n}, Nat.Coprime m n → f (m * n) = f m * f n)
    {V β : ℝ} (hβ : 0 ≤ β)
    (hsum : ∀ {p : ℕ}, p.Prime →
      Summable (fun j : ℕ => ‖f (p ^ j) * ((p ^ j : ℕ) : ℝ) ^ β‖))
    (N : ℕ) (s : Finset ℕ) (hs : ∀ n ∈ s, n ∈ N.smoothNumbers)
    (hlarge : ∀ n ∈ s, Real.exp V ≤ (n : ℝ)) :
    (∑ n ∈ s, f n) ≤ Real.exp (-β * V) *
      (∏ p ∈ N.primesBelow, ∑' j : ℕ, f (p ^ j) * ((p ^ j : ℕ) : ℝ) ^ β) := by
…

def OAI.Problem337.divisorHarmonicWeight line 77
Source documentation
The multiplicative weight occurring in divisor harmonic moments.
```
def divisorHarmonicWeight (r n : ℕ) : ℝ :=
…
```
theorem OAI.Problem337.divisorHarmonicWeight_nonneg line 80
theorem OAI.Problem337.divisorHarmonicWeight_one line 84
theorem OAI.Problem337.divisorHarmonicWeight_mul line 87
theorem OAI.Problem337.divisorHarmonicWeight_prime_power line 92
theorem OAI.Problem337.summable_successor_pow_geometric line 103
theorem OAI.Problem337.divisorHarmonicWeight_local_summable line 116

theorem OAI.Problem337.divisor_smooth_rankin_bound line 125

Source documentation

Concrete smooth-prefix Rankin estimate for any natural moment order.

theorem divisor_smooth_rankin_bound (r : ℕ) {V β : ℝ} (hβ : 0 ≤ β) (hβone : β < 1)
    (N : ℕ) (s : Finset ℕ) (hs : ∀ n ∈ s, n ∈ N.smoothNumbers)
    (hlarge : ∀ n ∈ s, Real.exp V ≤ (n : ℝ)) :
    (∑ n ∈ s, (n.divisors.card : ℝ) ^ r / (n : ℝ)) ≤ Real.exp (-β * V) *
      (∏ p ∈ N.primesBelow, ∑' j : ℕ,
        ((j + 1 : ℕ) : ℝ) ^ r * ((p : ℝ) ^ (β - 1)) ^ j) := by
…

theorem OAI.Problem337.divisor_harmonic_sum_le_euler_product line 144

Source documentation

The unweighted finite Euler-product bound for harmonic divisor moments.

theorem divisor_harmonic_sum_le_euler_product (r N : ℕ) (s : Finset ℕ)
    (hs : ∀ n ∈ s, n ∈ N.smoothNumbers) :
    (∑ n ∈ s, (n.divisors.card : ℝ) ^ r / (n : ℝ)) ≤
      ∏ p ∈ N.primesBelow, ∑' j : ℕ, ((j + 1 : ℕ) : ℝ) ^ r * ((p : ℝ)⁻¹) ^ j := by
…

def OAI.Problem337.divisorEulerFactor line 156
Source documentation
A local Euler factor, in the indexing convenient for Rankin's trick.
```
def divisorEulerFactor (r p : ℕ) (β : ℝ) : ℝ :=
…
```
theorem OAI.Problem337.divisorEulerFactor_one_le line 159

theorem OAI.Problem337.divisor_smooth_rankin_log_bound line 172

Source documentation

Logarithmic local-factor estimates turn the Rankin Euler product into a single exponential. This is the precise smooth-prefix bound used in the divisor-moment decomposition.

theorem divisor_smooth_rankin_log_bound (r : ℕ) {V β C : ℝ}
    (hβ : 0 ≤ β) (hβone : β < 1) (N : ℕ) (s : Finset ℕ)
    (hs : ∀ n ∈ s, n ∈ N.smoothNumbers)
    (hlarge : ∀ n ∈ s, Real.exp V ≤ (n : ℝ))
    (hlocal : ∀ p ∈ N.primesBelow,
      Real.log (divisorEulerFactor r p β) ≤ C * (p : ℝ) ^ (β - 1)) :
    (∑ n ∈ s, (n.divisors.card : ℝ) ^ r / (n : ℝ)) ≤
      Real.exp (-β * V + C * ∑ p ∈ N.primesBelow, (p : ℝ) ^ (β - 1)) := by
…

Mentions: OAI.Problem337.divisorEulerFactor