BoundaryGrid.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual finite boundary-box error in the prime mass comparison.

def OAI.TotientAsymptotic.witnessBandedRegion line 15
def OAI.TotientAsymptotic.witnessBoundaryGrid line 18
lemma OAI.TotientAsymptotic.gridBoundary_card_eq line 22
lemma OAI.TotientAsymptotic.gridBoundary_card_bound line 28
lemma OAI.TotientAsymptotic.witnessBoundaryGrid_crossing line 55
theorem OAI.TotientAsymptotic.weighted_boundary_grid_error line 72
Source documentation
The boundary-cardinality term appearing in the actual prime-grid sandwich has a vanishing normalized reciprocal-tail-weighted sum.
```
theorem weighted_boundary_grid_error (hbox : FordUnitPrimeBoxInput)
    (hmertens : MertensProductInput) (hren : FordRenewalInput)
    (hford : FordCoordinateConcentrationInput) :
    ∃ ε : ℕ → ℝ, Tendsto ε atTop (nhds 0) ∧
      ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
      (∑ d ∈ Finset.Icc 1 (tailValueBound H), (d : ℝ)⁻¹*
        (((gridOuter (bandGrid x H) (bandedWitnessRegion x H d)).card : ℝ)-
          (gridInner (bandGrid x H) (bandedWitnessRegion x H d)).card))/G x (m x) ≤ ε H := by
…
```
Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.FordCoordinateConcentrationInput, OAI.TotientAsymptotic.tailValueBound, OAI.TotientAsymptotic.gridOuter, OAI.TotientAsymptotic.bandGrid, OAI.TotientAsymptotic.bandedWitnessRegion, OAI.TotientAsymptotic.gridInner, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m