OAI/NumberTheory/TotientAsymptotic/BoundedRatioValues.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TotientAsymptotic.boundedRatioValues line 11
2. theorem OAI.TotientAsymptotic.bounded_ratio_positive_proportion line 16

   Source documentation

   The bounded-multiplier version of the published full-fiber construction retains the seed's strict margin above k.

   theorem bounded_ratio_positive_proportion {d k : ℕ} (hd : IsTotient d)
       (hseed : k*d < ell d) (hppt : PPTBoundedFiberPropagation d) :
       ∃ a b η : ℝ, (k : ℝ)<a ∧ 0<η ∧ 0<b ∧ ∀ᶠ x : ℝ in atTop,
         η*V x ≤ ((boundedRatioValues x a b).card : ℝ) := by
   …

   Mentions: OAI.TotientAsymptotic.IsTotient, OAI.TotientAsymptotic.ell, OAI.TotientAsymptotic.PPTBoundedFiberPropagation, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.boundedRatioValues