OAI/NumberTheory/JointDickman/Arithmetic/DeletedPrimeFactors.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The cost of deleting exceptional primes from a two-form sieve

  1. theorem OAI.JointDickman.inverse_square_le_singular line 15
  2. theorem OAI.JointDickman.delete_two_prime_sets line 36
  3. theorem OAI.JointDickman.deleted_divisor_factor_le line 63
  4. theorem OAI.JointDickman.large_divisor_inverse_square_bound line 83

    Source documentation

    Prime divisors above B^1000 have uniformly negligible reciprocal mass on every fixed logarithmic size range.

    theorem large_divisor_inverse_square_bound (κ : ℝ) :
    ∀ᶠ B : ℕ in atTop, ∀ (b : ℕ) (S : Finset ℕ), b ≠ 0 →
      (b : ℝ) ≤ Real.exp (κ * B) → S ⊆ b.primeFactors →
      (∀ p ∈ S, auxiliaryCutoff B ≤ p) →
      (∏ p ∈ S, (1 - 1 / (p : ℝ))⁻¹) ^ 2 ≤ Real.exp 1 := by
…

    Mentions: OAI.JointDickman.auxiliaryCutoff