OAI/NumberTheory/TotientAsymptotic/FullPrefixRatio.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TotientAsymptotic.tupleQ line 10
2. lemma OAI.TotientAsymptotic.tuple_least_ratio_identity line 13
3. lemma OAI.TotientAsymptotic.full_prefix_defect line 37

   Source documentation

   The product including the largest prime tends uniformly to one.

   lemma full_prefix_defect {ε : ℝ} (hε : 0<ε) :
       ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
         ∀ τ : TotientTuple (R x H), IsBasicTuple x H x τ →
           0<tupleQ τ ∧ 1-ε ≤ tupleQ τ ∧ tupleQ τ ≤ 1 := by
   …

   Mentions: OAI.TotientAsymptotic.TotientTuple, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.IsBasicTuple, OAI.TotientAsymptotic.tupleQ

4. lemma OAI.TotientAsymptotic.fk_lower_on_interval line 64