NormalInternalDiscard.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Sum every non-head normality failure, retaining all basic witnesses.

lemma OAI.TotientAsymptotic.nonnegative_sum_biUnion_le line 15
def OAI.TotientAsymptotic.nonNormalInternalRemainders line 27
lemma OAI.TotientAsymptotic.reverse_geometric_sum line 31
theorem OAI.TotientAsymptotic.normal_internal_reciprocal_discard line 56
Source documentation
This includes all positive prime coordinates for every retained normality scale, a larger family than the manuscript's short normality window.
```
theorem normal_internal_reciprocal_discard (hbox : FordUnitPrimeBoxInput)
    (hren : FordRenewalInput) (hmertens : MertensProductInput) (hford : FordLemma26Input) :
    ∃ ε : ℕ → ℝ, Tendsto ε atTop (nhds 0) ∧
      ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
        (∑ η ∈ nonNormalInternalRemainders x H, remainderReciprocalWeight η) ≤ ε H*G x (m x) := by
…
```
Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordLemma26Input, OAI.TotientAsymptotic.nonNormalInternalRemainders, OAI.TotientAsymptotic.remainderReciprocalWeight, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m