OAI/NumberTheory/TotientAsymptotic/ComparisonLargePart.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The largest-prime restriction supplies Ford's required part above Y₁.

  1. lemma OAI.TotientAsymptotic.comparison_small_part_cost line 14
  2. lemma OAI.TotientAsymptotic.prime_shift_log_lower line 32
  3. theorem OAI.TotientAsymptotic.comparison_large_prime_part line 49

    Source documentation

    The large prime part of the first shift exceeds sqrt y. The hypotheses are exactly the size consequences supplied by normality and the ordered grid.

    theorem comparison_large_prime_part : ∀ᶠ y : ℝ in atTop, ∀ p : ℕ, ∀ Z : ℝ,
    p.Prime → y^(9/10 : ℝ) ≤ p → 1 ≤ Z →
    Z ≤ Real.exp (Real.exp ((4/5 : ℝ)*B y)) →
    ((p-1).primeFactorsList.length : ℝ) ≤ 4*B y →
    Real.sqrt y < (partAbove (p-1) Z : ℝ) := by
…

    Mentions: OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.partAbove