MassUpper.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The actual arithmetic mass has the required uniform cofactor envelope.

lemma OAI.TotientAsymptotic.P_tendsto line 16
lemma OAI.TotientAsymptotic.P_lt_self line 20
def OAI.TotientAsymptotic.fullPrimeFactor line 31
lemma OAI.TotientAsymptotic.fullPrimeFactor_tendsto line 35
theorem OAI.TotientAsymptotic.mass_upper line 48
Source documentation
The manuscript's mass upper estimate, for every weight bounded above by one. Its only inputs are the published prime-box, renewal, and Mertens bounds.
```
theorem mass_upper (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput)
    (hmertens : MertensProductInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
      ∀ f : ℝ → ℝ, (∀ r, f r ≤ 1) →
        M x H f ≤ C*Real.exp ((4*(lam/rho))*cofactorScale H)*G x (m x) := by
…
```
Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.M, OAI.TotientAsymptotic.lam, OAI.TotientAsymptotic.rho, OAI.TotientAsymptotic.cofactorScale, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m