OAI/NumberTheory/TotientAsymptotic/IntervalAvoidance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Ford's interval-avoidance sieve, with natural-number endpoints.

  1. lemma OAI.TotientAsymptotic.intervalSifted_card_le line 11
  2. lemma OAI.TotientAsymptotic.intervalSifted_antitone line 15
  3. lemma OAI.TotientAsymptotic.mem_intervalSifted line 26
  4. theorem OAI.TotientAsymptotic.interval_avoidance_count line 50

    Source documentation

    All cutoffs are uniform. The proof only uses the already proved concrete Selberg error, finite Euler product, and explicit small-power cutoff.

    theorem interval_avoidance_count : ∃ C : ℝ,0 < C ∧ ∀ S X z : ℕ,
    2 ≤ S → S ≤ z → z ≤ X →
      ((intervalSifted S X z).card:ℝ) ≤ C*X*Real.log S/Real.log z := by
…

    Mentions: OAI.TotientAsymptotic.intervalSifted