PrimeReciprocalSharp.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.nat_rpow_series_le line 11
Source documentation
The elementary integral estimate for the real zeta series.
```
theorem nat_rpow_series_le {s : ℝ} (hs : 1 < s) :
    (∑' n : ℕ, (n : ℝ) ^ (-s)) ≤ 1 + 1 / (s - 1) := by
…
```

theorem OAI.Problem337.prime_rpow_sum_le_log_zeta_bound line 41

Source documentation

A finite-prime Euler-product estimate, without any prime-distribution input.

theorem prime_rpow_sum_le_log_zeta_bound (P : Finset ℕ)
    (hP : ∀ p ∈ P, p.Prime) {s : ℝ} (hs : 1 < s) :
    (∑ p ∈ P, (p : ℝ) ^ (-s)) ≤ Real.log (1 + 1 / (s - 1)) := by
…

theorem OAI.Problem337.prime_reciprocal_sum_le line 79

Source documentation

The elementary logarithmic bound for reciprocals of primes in a finite interval.

theorem prime_reciprocal_sum_le (P : Finset ℕ) (T : ℝ) (hT : 2 ≤ T)
    (hP : ∀ p ∈ P, p.Prime) (hcap : ∀ p ∈ P, (p : ℝ) ≤ T) :
    (∑ p ∈ P, 1 / (p : ℝ)) ≤ Real.exp 1 * Real.log (1 + Real.log T) := by
…

theorem OAI.Problem337.prime_weighted_reciprocal_sum_le line 113

Source documentation

The weighted variant used in the smooth-prefix divisor estimate.

theorem prime_weighted_reciprocal_sum_le (P : Finset ℕ) (T δ : ℝ)
    (hT : 2 ≤ T) (hδ : 0 ≤ δ) (hP : ∀ p ∈ P, p.Prime)
    (hcap : ∀ p ∈ P, (p : ℝ) ≤ T) :
    (∑ p ∈ P, (p : ℝ) ^ (-1 + δ)) ≤
      T ^ δ * Real.exp 1 * Real.log (1 + Real.log T) := by
…