OmegaInternalDiscard.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite layer summation for the remaining-factor exclusion.

def OAI.TotientAsymptotic.omegaInternalRemainders line 16
theorem OAI.TotientAsymptotic.omega_internal_reciprocal_discard line 21
Source documentation
Sum all exceptional factor-count coordinates after each actual collision cutoff.
```
theorem omega_internal_reciprocal_discard (hbox : FordUnitPrimeBoxInput)
    (hren : FordRenewalInput) (hmertens : MertensProductInput) :
    ∃ ε : ℕ → ℝ, Tendsto ε atTop (nhds 0) ∧
      ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
        (∑ η ∈ omegaInternalRemainders x H, remainderReciprocalWeight η) ≤ ε H*G x (m x) := by
…
```
Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.omegaInternalRemainders, OAI.TotientAsymptotic.remainderReciprocalWeight, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m