NormalityDiscard.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The complete normality exclusion for the actual universally good tuples.

def OAI.TotientAsymptotic.nonNormalInternalTuples line 15
def OAI.TotientAsymptotic.FailsWitnessNormality line 19
def OAI.TotientAsymptotic.normalityFailureTuples line 23
lemma OAI.TotientAsymptotic.nonNormalInternalRemainders_basic line 27
lemma OAI.TotientAsymptotic.nonNormalInternalTuples_card_le line 34
lemma OAI.TotientAsymptotic.normalityFailureTuples_subset line 51
theorem OAI.TotientAsymptotic.normality_tuple_discard line 73
Source documentation
Normality is required for every full basic witness, including alternate witnesses of the same tuple. The whole excluded tuple family is negligible.
```
theorem normality_tuple_discard (hbox : FordUnitPrimeBoxInput)
    (hren : FordRenewalInput) (hmertens : MertensProductInput) (hford : FordLemma26Input) :
    ∃ ε : ℕ → ℝ, Tendsto ε atTop (nhds 0) ∧
      ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop, ∀ t ≤ x,
        ((normalityFailureTuples x H t).card : ℝ) ≤ ε H*(x/Real.log x*G x (m x)) := by
…
```
Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordLemma26Input, OAI.TotientAsymptotic.normalityFailureTuples, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m