SmoothResidualMass.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The finite Euler product bounds the entire smooth residual-integer sum.

def OAI.TotientAsymptotic.reciprocalNatHom line 14
lemma OAI.TotientAsymptotic.prime_reciprocal_norm_lt_one line 19
lemma OAI.TotientAsymptotic.reciprocal_prime_factor line 24
theorem OAI.TotientAsymptotic.smooth_residual_reciprocal_mass line 32
Source documentation
Only positivity and smoothness are used; the residuals may repeat prime factors and the upper cutoff on their size is arbitrary.
```
theorem smooth_residual_reciprocal_mass (N : ℕ) (Q : Finset ℕ)
    (hQ : ∀ n ∈ Q, 0 < n ∧ largestPrimeFactor n ≤ N) :
    (∑ n ∈ Q, (n : ℝ)⁻¹) ≤ primeEulerProduct N := by
…
```
Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.largestPrimeFactor, OAI.TotientAsymptotic.primeEulerProduct
theorem OAI.TotientAsymptotic.smooth_residual_mass_mertens line 68