SubcriticalPowerSum.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.DivisorMoment.shifted_power_sum_le line 9

Source documentation

Integral comparison for a subcritical power, beginning at the integer two.

theorem shifted_power_sum_le (n : ℕ) {α : ℝ} (hα0 : 0 < α) (hα1 : α ≤ 1) :
    (∑ j ∈ Finset.range n, ((j : ℝ) + 2) ^ (α - 1)) ≤
      (((n : ℝ) + 1) ^ α - 1) / α := by
…

theorem OAI.Problem337.DivisorMoment.shifted_power_sum_le_div line 26

Source documentation

Convenient coarse form of the same estimate.

theorem shifted_power_sum_le_div (n : ℕ) {α : ℝ} (hα0 : 0 < α) (hα1 : α ≤ 1) :
    (∑ j ∈ Finset.range n, ((j : ℝ) + 2) ^ (α - 1)) ≤
      ((n : ℝ) + 1) ^ α / α := by
…

theorem OAI.Problem337.DivisorMoment.finite_power_sum_le line 33

Source documentation

Any collection of integers in [2,T] obeys the same subcritical power bound.

theorem finite_power_sum_le (T : ℕ) (s : Finset ℕ)
    (hs : ∀ a ∈ s, 2 ≤ a ∧ a ≤ T)
    {α : ℝ} (hα0 : 0 < α) (hα1 : α ≤ 1) :
    (∑ a ∈ s, (a : ℝ) ^ (α - 1)) ≤ ((T : ℝ) + 1) ^ α / α := by
…

theorem OAI.Problem337.DivisorMoment.log_inv_one_sub_le line 54
Source documentation
A uniform elementary logarithmic bound for geometric Euler factors.
```
theorem log_inv_one_sub_le {x ρ : ℝ} (hx0 : 0 ≤ x) (hxρ : x ≤ ρ) (hρ : ρ < 1) :
    Real.log ((1 - x)⁻¹) ≤ x / (1 - ρ) := by
…
```

theorem OAI.Problem337.DivisorMoment.log_geometric_product_le line 65

Source documentation

Logarithm of a finite geometric Euler product, requiring only a≥2, not primality.

theorem log_geometric_product_le (T : ℕ) (s : Finset ℕ)
    (hs : ∀ a ∈ s, 2 ≤ a ∧ a ≤ T)
    {α : ℝ} (hα0 : 0 < α) (hα1 : α < 1) :
    Real.log (∏ a ∈ s, (1 - (a : ℝ) ^ (α - 1))⁻¹) ≤
      ((T : ℝ) + 1) ^ α / (α * (1 - (2 : ℝ) ^ (α - 1))) := by
…

theorem OAI.Problem337.DivisorMoment.log_geometric_product_le_real line 95

Source documentation

Real cutoff version of the geometric Euler-product estimate.

theorem log_geometric_product_le_real {U : ℝ} (hU : 1 ≤ U) (s : Finset ℕ)
    (hs : ∀ a ∈ s, 2 ≤ a ∧ (a : ℝ) ≤ U)
    {α : ℝ} (hα0 : 0 < α) (hα1 : α < 1) :
    Real.log (∏ a ∈ s, (1 - (a : ℝ) ^ (α - 1))⁻¹) ≤
      ((2 : ℝ) ^ α / (α * (1 - (2 : ℝ) ^ (α - 1)))) * U ^ α := by
…

theorem OAI.Problem337.DivisorMoment.small_prime_rankin_product_log_bound line 121

Source documentation

The small-prime Rankin product grows at most exponentially in S^(2/5). No primality hypothesis is needed, since summing over all integers is an upper bound.

theorem small_prime_rankin_product_log_bound :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : ℝ), 1 ≤ S → ∀ s : Finset ℕ,
      (∀ p ∈ s, 2 ≤ p ∧ (p : ℝ) ≤ S ^ (4 : ℕ)) →
      Real.log (∏ p ∈ s, (1 - (p : ℝ) ^ (-(9 / 10 : ℝ)))⁻¹) ≤
        C * S ^ (2 / 5 : ℝ) := by
…