BandPrimeError.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

A dimension-independent prime-box error from the retained lower bands.

lemma OAI.TotientAsymptotic.bandScale_lower line 14
lemma OAI.TotientAsymptotic.sum_reverse_geometric line 25
lemma OAI.TotientAsymptotic.sum_exp_neg_bandScale_le line 46
def OAI.TotientAsymptotic.bandPrimeError line 74
lemma OAI.TotientAsymptotic.bandPrimeError_tendsto line 77
theorem OAI.TotientAsymptotic.banded_grid_prime_mass_error line 93
Source documentation
On any finite union of boxes above the retained lower bands, prime mass and volume have a relative error tending to zero with the tail cut. The bound is uniform in x, the number of prefix coordinates, and the phase.
```
theorem banded_grid_prime_mass_error (hford : FordUnitPrimeBoxInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ {x c : ℝ} {H : ℕ}, 0 ≤ theta x → 0 < c → H ≤ m x →
      ∀ K : Finset (Fin (R x H) → ℕ),
        (∀ b ∈ K, ∀ i, 1 ≤ b i ∧ c*bandScale x (i.val+1) ≤ b i) →
        |gridPrimeMass K-(MeasureTheory.volume (gridRegion K)).toReal| ≤
          (MeasureTheory.volume (gridRegion K)).toReal*bandPrimeError C c H := by
…
```
Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.bandScale, OAI.TotientAsymptotic.gridPrimeMass, OAI.TotientAsymptotic.gridRegion, OAI.TotientAsymptotic.bandPrimeError