UnionPerturbation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Perturbation removal for the actual unions in the finite coefficient.

lemma OAI.TotientAsymptotic.prefixBandRegion_volume_ne_top line 15
lemma OAI.TotientAsymptotic.union_perturbation_loss_bound line 21
theorem OAI.TotientAsymptotic.weighted_union_perturbation_removal line 49
Source documentation
Removing all retained xi factors in the actual witness unions has a vanishing normalized error for every weight between zero and one.
```
theorem weighted_union_perturbation_removal (hbox : FordUnitPrimeBoxInput)
    (hmertens : MertensProductInput) (hren : FordRenewalInput) :
    ∃ ε : ℕ → ℝ, Tendsto ε atTop (nhds 0) ∧
      ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
      ∀ f : ℝ → ℝ, (∀ r, 0 ≤ f r ∧ f r ≤ 1) →
      (∑ d ∈ Finset.Icc 1 (tailValueBound H), f ((ell d : ℝ)/d)/d *
        volume.real ((⋃ η ∈ witnessFinset H (theta x) d,
          perturbedTailPrefixRegion x H η ∩ prefixBandRegion x H) \
            (⋃ η ∈ witnessFinset H (theta x) d, tailPrefixRegion x H η)))/G x (m x) ≤ ε H := by
…
```
Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.tailValueBound, OAI.TotientAsymptotic.ell, OAI.TotientAsymptotic.witnessFinset, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.perturbedTailPrefixRegion, OAI.TotientAsymptotic.prefixBandRegion, OAI.TotientAsymptotic.tailPrefixRegion, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m