BandGrid.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite grids covering the actual arithmetic prefix fibers.

def OAI.TotientAsymptotic.bandGrid line 14
lemma OAI.TotientAsymptotic.bandGrid_bounds line 19
lemma OAI.TotientAsymptotic.prefixBandRegion_covered line 24
def OAI.TotientAsymptotic.bandedWitnessRegion line 44
lemma OAI.TotientAsymptotic.prefixDatum_iff_prime_region line 47
theorem OAI.TotientAsymptotic.prefixPrimeFiber_eq_grid line 61
Source documentation
The actual finite prefix fiber is a restricted prime-box grid, with one copy of each prefix even if several witnesses permit it.
```
theorem prefixPrimeFiber_eq_grid {x : ℝ} {H d : ℕ}
    (hPH : P H < H) (hHm : H ≤ m x) :
    prefixPrimeFiber x H d = (gridPrimeTuples (bandGrid x H)).filter
      (fun p => primePrefixCoord p ∈ bandedWitnessRegion x H d) := by
…
```
Mentions: OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.prefixPrimeFiber, OAI.TotientAsymptotic.gridPrimeTuples, OAI.TotientAsymptotic.bandGrid, OAI.TotientAsymptotic.primePrefixCoord, OAI.TotientAsymptotic.bandedWitnessRegion
theorem OAI.TotientAsymptotic.mass_eq_banded_grid_sum line 76
Source documentation
Exact conversion of the arithmetic mass to the bounded grid regions. All subsequent estimates act on these regions, not on a count of witnesses.
```
theorem mass_eq_banded_grid_sum {x : ℝ} {H : ℕ}
    (hPH : P H < H) (hHm : H ≤ m x) (hs : theta x ∈ Set.Ico (0 : ℝ) 1)
    (f : ℝ → ℝ) :
    M x H f = ∑ d ∈ Finset.Icc 1 (tailValueBound H), f ((ell d : ℝ)/d)/d *
      gridRestrictedPrimeMass (bandGrid x H) (bandedWitnessRegion x H d) := by
…
```
Mentions: OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.M, OAI.TotientAsymptotic.tailValueBound, OAI.TotientAsymptotic.ell, OAI.TotientAsymptotic.gridRestrictedPrimeMass, OAI.TotientAsymptotic.bandGrid, OAI.TotientAsymptotic.bandedWitnessRegion