UniformPrefactor.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

A simultaneous bound for all projected prefix volumes.

lemma OAI.TotientAsymptotic.inverse_scale_eq line 13
lemma OAI.TotientAsymptotic.inverse_scale_bound line 20
lemma OAI.TotientAsymptotic.uniform_step_bound line 35
theorem OAI.TotientAsymptotic.uniform_projected_volume_bound line 67
Source documentation
Ford's bounded renewal error yields the manuscript's simultaneous projected-volume majorant, including prefixes whose length moves with x.
```
theorem uniform_projected_volume_bound (hford : FordRenewalInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ x : ℝ in atTop, ∀ H ≤ m x,
      G x (m x-H)/G x (m x) ≤ C^H*rho^(H*(H-1)/2) := by
…
```
Mentions: OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.rho
def OAI.TotientAsymptotic.projectedEnvelope line 87
lemma OAI.TotientAsymptotic.summable_projectedEnvelope line 89