PerturbationRemoval.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Removing the perturbed prefix inequalities with their full arithmetic weights.

theorem OAI.TotientAsymptotic.witness_perturbation_removal line 18
Source documentation
All xi-perturbations in the retained prefix have negligible total weighted volume, uniformly over every finite family of actual witnesses.
```
theorem witness_perturbation_removal (hbox : FordUnitPrimeBoxInput)
    (hmertens : MertensProductInput) (hren : FordRenewalInput) :
    ∃ ε : ℕ → ℝ, Tendsto ε atTop (nhds 0) ∧
      ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
      ∀ W : Finset (TailDatum H), (∀ η ∈ W, IsWitness H (theta x) η) →
      (∑ η ∈ W, ((w η).totient : ℝ)⁻¹*
        volume.real ((perturbedTailPrefixRegion x H η ∩ prefixBandRegion x H) \
          tailPrefixRegion x H η))/G x (m x) ≤ ε H := by
…
```
Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.TailDatum, OAI.TotientAsymptotic.IsWitness, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.w, OAI.TotientAsymptotic.perturbedTailPrefixRegion, OAI.TotientAsymptotic.prefixBandRegion, OAI.TotientAsymptotic.tailPrefixRegion, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m