OAI/NumberTheory/TotientAsymptotic/ValueOmega.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TotientAsymptotic.largeOmegaValues line 13
2. theorem OAI.TotientAsymptotic.large_omega_value_count line 18

   Source documentation

   A deliberately coarse factor-count cutoff still has vanishing relative cost and supplies the head-prime lower bound in every remaining preimage.

   theorem large_omega_value_count (hmertens : MertensProductInput) :
       ∃ C : ℝ, 0 < C ∧ ∀ᶠ x : ℝ in atTop,
         ((largeOmegaValues x).card : ℝ) ≤ (C/Real.log x)*(x/Real.log x) := by
   …

   Mentions: OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.largeOmegaValues