OAI/NumberTheory/TotientAsymptotic/PositiveTupleWeight.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.bounded_ratio_tuple_weight line 13
2. lemma OAI.TotientAsymptotic.positive_weighted_tuple_count line 51

   Source documentation

   A published positive family survives the exceptional-value discard and has a positive, uniformly bounded-below tuple weight.

   lemma positive_weighted_tuple_count (hscale : FordScaleBounds)
       (hstruct : ExtractedStructureInput)
       (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) (hmertens : MertensProductInput)
       (h26 : FordLemma26Input) (h51 : FordLemma51Input)
       {d k : ℕ} (hd : IsTotient d) (hseed : k*d<ell d) (hppt : PPTBoundedFiberPropagation d) :
       ∃ c : ℝ, 0<c ∧ ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
         c*tupleNormalization x ≤ weightedTupleCount x H x (fk k) := by
   …

   Mentions: OAI.TotientAsymptotic.FordScaleBounds, OAI.TotientAsymptotic.ExtractedStructureInput, OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordLemma26Input, OAI.TotientAsymptotic.FordLemma51Input, OAI.TotientAsymptotic.IsTotient, OAI.TotientAsymptotic.ell, OAI.TotientAsymptotic.PPTBoundedFiberPropagation, OAI.TotientAsymptotic.weightedTupleCount, OAI.TotientAsymptotic.fk