OAI/NumberTheory/JointDickman/Arithmetic/LargeDivisorReciprocals.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.prime_divisor_card_log line 10
2. theorem OAI.JointDickman.large_prime_divisor_reciprocals line 24

   Source documentation

   Only logarithmic size, nonvanishing, and the prime cutoff are needed. This applies both to forced third-site roots and to cross-root collisions.

   theorem large_prime_divisor_reciprocals {b : ℤ} (hb : b ≠ 0)
       (S : Finset ℕ) (hS : S ⊆ b.natAbs.primeFactors)
       {P H : ℝ} (hP : 0 < P) (hcut : ∀ p ∈ S, P ≤ (p : ℝ))
       (hsize : (b.natAbs : ℝ) ≤ Real.exp H) :
       ∑ p ∈ S, 1/(p : ℝ) ≤ H/(Real.log 2*P) := by
   …