OuterGrid.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A uniform majorant for the outer boxes in the prime-volume sandwich.

lemma OAI.TotientAsymptotic.fullBoxSimplex_volume_bound line 15
lemma OAI.TotientAsymptotic.outer_grid_union_card line 37
theorem OAI.TotientAsymptotic.outer_grid_mass_bound line 53
Source documentation
The whole outer-box volume has only the subpolynomial cofactor cost.
```
theorem outer_grid_mass_bound (hbox : FordUnitPrimeBoxInput)
    (hmertens : MertensProductInput) (hren : FordRenewalInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
      (∑ d ∈ Finset.Icc 1 (tailValueBound H), (d : ℝ)⁻¹*
        (gridOuter (bandGrid x H) (bandedWitnessRegion x H d)).card) ≤
      C*Real.exp ((4*(lam/rho))*cofactorScale H)*G x (m x) := by
…
```
Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.tailValueBound, OAI.TotientAsymptotic.gridOuter, OAI.TotientAsymptotic.bandGrid, OAI.TotientAsymptotic.bandedWitnessRegion, OAI.TotientAsymptotic.lam, OAI.TotientAsymptotic.rho, OAI.TotientAsymptotic.cofactorScale, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m