OAI/NumberTheory/TotientAsymptotic/CofactorDiscard.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TotientAsymptotic.oversized_cofactor_count line 14

   Source documentation

   Any finite family of preimages with oversized smooth cofactors has vanishing normalized size. The family may be chosen from actual bad values.

   theorem oversized_cofactor_count (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput)
       (hmertens : MertensProductInput) :
       ∃ ε : ℕ → ℝ, Tendsto ε atTop (nhds 0) ∧
         ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
         ∀ S : Finset (RemainderDatum (L x H) × ℕ),
         (∀ q ∈ S, IsUntruncatedRemainder x H q.1 ∧ q.2.Prime ∧
           x^(9/10 : ℝ) ≤ q.2 ∧ ((wholePreimage q.2 q.1).totient : ℝ) ≤ x ∧
           Real.exp (2*bandScale x (L x H)) < Real.log q.1.cofactor) →
         (S.card : ℝ) ≤ ε H*tupleNormalization x := by
   …

   Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.IsUntruncatedRemainder, OAI.TotientAsymptotic.wholePreimage, OAI.TotientAsymptotic.bandScale