WitnessUnionLoss.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Transfer of the band-removal estimate to the actual unions at each tail value.

def OAI.TotientAsymptotic.activeWitnesses line 14
lemma OAI.TotientAsymptotic.mem_activeWitnesses line 17
lemma OAI.TotientAsymptotic.sum_witness_fibers line 22
lemma OAI.TotientAsymptotic.weighted_witness_fibers line 40
lemma OAI.TotientAsymptotic.union_band_loss_bound line 53
theorem OAI.TotientAsymptotic.weighted_union_band_removal line 70
Source documentation
The discarded volume in the coefficient's actual witness unions is uniformly negligible for every weight between zero and one.
```
theorem weighted_union_band_removal (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) →
      (∑ d ∈ Finset.Icc 1 (tailValueBound H), f ((ell d : ℝ)/d)/d *
        volume.real ((⋃ η ∈ witnessFinset H (theta x) d, tailPrefixRegion x H η) \
          prefixBandRegion x H))/G x (m x) ≤ ε H := by
…
```
Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.FordCoordinateConcentrationInput, OAI.TotientAsymptotic.tailValueBound, OAI.TotientAsymptotic.ell, OAI.TotientAsymptotic.witnessFinset, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.tailPrefixRegion, OAI.TotientAsymptotic.prefixBandRegion, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m