OAI/NumberTheory/TotientAsymptotic/FordHead.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.first_band_small line 12
2. lemma OAI.TotientAsymptotic.ford_rest_le_power line 29
3. lemma OAI.TotientAsymptotic.ford_log_factorization line 43
4. lemma OAI.TotientAsymptotic.head_remainder_log_error line 59
5. theorem OAI.TotientAsymptotic.extracted_head_large line 71

   Source documentation

   All preimages outside the small-value and high-Omega sets have a head prime in the required range. The constants leave room for the coarse bands.

   theorem extracted_head_large : ∀ᶠ x : ℝ in atTop, ∀ H n : ℕ,
       0 < L x H → 0 < n → extractedStructureCondition x (P H) n →
       x^(19/20 : ℝ) ≤ n.totient → (n.totient.primeFactorsList.length : ℝ) ≤ 20*B x →
       x^(9/10 : ℝ) ≤ fordPrime n 0 := by
   …

   Mentions: OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.extractedStructureCondition, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.fordPrime