GridApproximation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Prime mass versus volume, with all remaining error confined to boundary boxes.

lemma OAI.TotientAsymptotic.gridInner_region_subset line 15
lemma OAI.TotientAsymptotic.gridOuter_region_covers line 22
lemma OAI.TotientAsymptotic.grid_volume_sandwich line 30
lemma OAI.TotientAsymptotic.grid_restricted_mass_error line 45
lemma OAI.TotientAsymptotic.bandPrimeError_nonneg line 61
theorem OAI.TotientAsymptotic.banded_restricted_mass_error line 72
Source documentation
For every subset of the retained bands, the only error beyond the prime box estimate is the number of boxes crossing its boundary.
```
theorem banded_restricted_mass_error (hford : FordUnitPrimeBoxInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ {x : ℝ} {H : ℕ}, 0 ≤ theta x → H ≤ m x →
      ∀ S : Set (Fin (R x H) → ℝ), S ⊆ prefixBandRegion x H →
      |gridRestrictedPrimeMass (bandGrid x H) S-(volume S).toReal| ≤
        (gridOuter (bandGrid x H) S).card*bandPrimeError C (9/10) H+
          ((gridOuter (bandGrid x H) S).card-(gridInner (bandGrid x H) S).card) := by
…
```
Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.prefixBandRegion, OAI.TotientAsymptotic.gridRestrictedPrimeMass, OAI.TotientAsymptotic.bandGrid, OAI.TotientAsymptotic.gridOuter, OAI.TotientAsymptotic.bandPrimeError, OAI.TotientAsymptotic.gridInner
def OAI.TotientAsymptotic.bandedVolumeMass line 89

theorem OAI.TotientAsymptotic.mass_banded_volume_error line 95

Source documentation

A finite quantitative mass-to-volume estimate for the genuine witness unions. The bound is uniform over weights between zero and one.

theorem mass_banded_volume_error (hford : FordUnitPrimeBoxInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ {x : ℝ} {H : ℕ}, P H < H → H ≤ m x →
      theta x ∈ Set.Ico (0 : ℝ) 1 → ∀ f : ℝ → ℝ,
      (∀ r, 0 ≤ f r ∧ f r ≤ 1) →
      |M x H f-bandedVolumeMass x H f| ≤
        ∑ d ∈ Finset.Icc 1 (tailValueBound H), (d : ℝ)⁻¹*
          ((gridOuter (bandGrid x H) (bandedWitnessRegion x H d)).card*bandPrimeError C (9/10) H+
            ((gridOuter (bandGrid x H) (bandedWitnessRegion x H d)).card-
              (gridInner (bandGrid x H) (bandedWitnessRegion x H d)).card)) := by
…

Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.M, OAI.TotientAsymptotic.bandedVolumeMass, OAI.TotientAsymptotic.tailValueBound, OAI.TotientAsymptotic.gridOuter, OAI.TotientAsymptotic.bandGrid, OAI.TotientAsymptotic.bandedWitnessRegion, OAI.TotientAsymptotic.bandPrimeError, OAI.TotientAsymptotic.gridInner