OAI/NumberTheory/TwoPoint/Bounds/PrimeCountDilation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Extracting x=u*z from the core-prime cutoff. Primes excluded because they divide u do not reappear in the count, even at exceptional integers where the multiplicative functions themselves cannot yet be factored.

  1. lemma OAI.TwoPointCorrelations.finitePrimeDivisorCount_mul_of_avoids line 14
  2. lemma OAI.TwoPointCorrelations.finitePrimeDivisorCount_filter_mul line 22
  3. lemma OAI.TwoPointCorrelations.finitePrimeDivisorCount_same_core_factors line 34

    Source documentation

    The expanded divisor d and retained divisor u have the same core prime factors, so the core cutoff depends only on the reduced variable.

    lemma finitePrimeDivisorCount_same_core_factors (C : Finset ℕ)
    (hC : ∀ p ∈ C, Nat.Prime p) (d u n : ℕ)
    (hcore : ∀ p ∈ C, p ∣ d ↔ p ∣ u) :
    finitePrimeDivisorCount (C.filter (fun p => ¬p ∣ d)) (u * n) =
      finitePrimeDivisorCount (C.filter (fun p => ¬p ∣ u)) n := by
…

    Mentions: OAI.TwoPointCorrelations.finitePrimeDivisorCount

  4. lemma OAI.TwoPointCorrelations.primeCountCutoff_same_core_factors line 46