VolumeComparison.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The banded perturbed volume and the exact finite coefficient differ by a vanishing normalized error.

def OAI.TotientAsymptotic.exactWitnessUnion line 15
def OAI.TotientAsymptotic.perturbedWitnessUnion line 18
lemma OAI.TotientAsymptotic.bandedWitnessRegion_eq line 22
lemma OAI.TotientAsymptotic.exactWitnessUnion_volume_ne_top line 33
lemma OAI.TotientAsymptotic.perturbedWitnessUnion_volume_ne_top line 38
lemma OAI.TotientAsymptotic.exactWitnessUnion_empty_of_not_totient line 47
lemma OAI.TotientAsymptotic.unionVolumeCoefficient_mul_G line 57
lemma OAI.TotientAsymptotic.perturbed_exact_volume_difference line 72
theorem OAI.TotientAsymptotic.banded_volume_coefficient_approximation line 99
Source documentation
The geometric approximation to the exact coefficient. Only the prime-grid-to-volume step remains in the mass approximation after this.
```
theorem banded_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) →
      |bandedVolumeMass 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.bandedVolumeMass, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.unionVolumeCoefficient