MassVolumeApproximation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual arithmetic prime mass approximates the exact witness-union volume, uniformly in all bounded nonnegative weights.

theorem OAI.TotientAsymptotic.mass_banded_volume_approximation line 14
theorem OAI.TotientAsymptotic.mass_volume_coefficient_approximation line 68
Source documentation
The complete mass-to-union-volume estimate, including removal of the prime grid, all prefix perturbations, and all retained bands.
```
theorem mass_volume_coefficient_approximation (hbox : FordUnitPrimeBoxInput)
    (hmertens : MertensProductInput) (hren : FordRenewalInput)
    (hford : FordCoordinateConcentrationInput) :
    ∃ δ : ℕ → ℝ, Tendsto δ atTop (nhds 0) ∧
      ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
      ∀ f : ℝ → ℝ, (∀ r, 0 ≤ f r ∧ f r ≤ 1) →
      |M x H f/G x (m x)-unionVolumeCoefficient H f x| ≤ δ H := by
…
```
Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.FordCoordinateConcentrationInput, OAI.TotientAsymptotic.M, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.unionVolumeCoefficient
theorem OAI.TotientAsymptotic.mass_finite_coefficient_approximation line 86
Source documentation
The manuscript's finite arithmetic coefficient approximates each fixed bounded nonnegative weight, with an error vanishing as the tail cut grows.
```
theorem mass_finite_coefficient_approximation (hbox : FordUnitPrimeBoxInput)
    (hmertens : MertensProductInput) (hren : FordRenewalInput)
    (hford : FordCoordinateConcentrationInput) :
    ∃ δ : ℕ → ℝ, Tendsto δ atTop (nhds 0) ∧
      ∀ᶠ H : ℕ in atTop, ∀ f : ℝ → ℝ, (∀ r, 0 ≤ f r ∧ f r ≤ 1) →
      ∀ ε : ℝ, 0 < ε → ∀ᶠ x : ℝ in atTop,
        |M x H f/G x (m x)-AH H f (theta x)| ≤ δ H+ε := by
…
```
Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.FordCoordinateConcentrationInput, OAI.TotientAsymptotic.M, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.AH, OAI.TotientAsymptotic.theta