BandRemoval.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Removing the retained bands after aggregating complete witness boxes.

lemma OAI.TotientAsymptotic.measurableSet_prefixBandRegion line 16
lemma OAI.TotientAsymptotic.fullBoxSimplex_volume_ne_top line 24
lemma OAI.TotientAsymptotic.retainedPhaseBad_volume_ne_top line 35
lemma OAI.TotientAsymptotic.eventually_scale_product_lower line 43
lemma OAI.TotientAsymptotic.band_loss_enclosure line 55
theorem OAI.TotientAsymptotic.witness_band_removal line 89
Source documentation
The entire reciprocal-totient weighted loss from removing retained bands is negligible, uniformly over finite families of actual witnesses.
```
theorem witness_band_removal (hbox : FordUnitPrimeBoxInput)
    (hmertens : MertensProductInput) (hren : FordRenewalInput)
    (hford : FordCoordinateConcentrationInput) :
    ∃ ε : ℕ → ℝ, Tendsto ε atTop (nhds 0) ∧
      ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
      ∀ W : Finset (TailDatum H), (∀ η ∈ W, IsWitness H (theta x) η) →
      (∑ η ∈ W, ((w η).totient : ℝ)⁻¹*
        volume.real (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.TailDatum, OAI.TotientAsymptotic.IsWitness, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.w, OAI.TotientAsymptotic.tailPrefixRegion, OAI.TotientAsymptotic.prefixBandRegion, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m