TailCofactor.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The uniform reciprocal cofactor envelope at the discrete tail cut.

def OAI.TotientAsymptotic.exponentialCofactorCap line 12
lemma OAI.TotientAsymptotic.exponentialCofactorCap_bounds line 14
theorem OAI.TotientAsymptotic.exponential_cofactor_sum line 31
theorem OAI.TotientAsymptotic.tail_cofactor_sum line 54
Source documentation
The entire allowed cofactor sum has the manuscript's exponential envelope in P rho^(-P), uniformly over the phase.
```
theorem tail_cofactor_sum (hmertens : MertensProductInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ H : ℕ,
      (∑ a ∈ Finset.Icc 1 (tailCofactorBound H), (a.totient : ℝ)⁻¹) ≤
        C*Real.exp (4*(lam/rho)*(P H : ℝ)*(rho^(P H))⁻¹) := by
…
```
Mentions: OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.tailCofactorBound, OAI.TotientAsymptotic.lam, OAI.TotientAsymptotic.rho, OAI.TotientAsymptotic.P