MertensLogMass.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A finite summation-by-parts bound sufficient for the Mertens product.

lemma OAI.TotientAsymptotic.weighted_sum_le_harmonic line 11
lemma OAI.TotientAsymptotic.prime_log_mass_le line 52
Source documentation
Only a coarse logarithmic bound is needed; no Mertens theorem is assumed.
```
lemma prime_log_mass_le (N : ℕ) (hN : 2 ≤ N) :
    (∑ p ∈ (Finset.Icc 2 N).filter Nat.Prime, Real.log p/(p : ℝ)) ≤
      Real.log 4*(2+Real.log N) := by
…
```
Mentions: OAI.TotientAsymptotic.N