CanceledPrimeMass.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The reciprocal cost of fixing the canceled primes, from Mertens' input.

lemma OAI.TotientAsymptotic.prime_shift_inv_le_log_factor line 12
lemma OAI.TotientAsymptotic.primeEulerProduct_pos line 26
lemma OAI.TotientAsymptotic.canceled_prime_mass_le_log_product line 33
theorem OAI.TotientAsymptotic.canceled_prime_mass_mertens line 50
Source documentation
A canceled prime costs only the logarithm of the prime-product bound, which is of double-logarithmic size in its allowed prime endpoint.
```
theorem canceled_prime_mass_mertens (hmertens : MertensProductInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ N : ℕ, 2 ≤ N →
      (∑ p ∈ (Finset.Icc 2 N).filter Nat.Prime, ((p-1 : ℕ) : ℝ)⁻¹) ≤
        2*(Real.log C+B N) := by
…
```
Mentions: OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.B