OAI/NumberTheory/JointDickman/Arithmetic/TotientDivisorBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A divisor majorant for the totient correction

  1. lemma OAI.JointDickman.prime_subset_reciprocal_product_le_divisors line 10
  2. lemma OAI.JointDickman.totient_ratio_prime_product line 40
  3. theorem OAI.JointDickman.totient_ratio_le_divisor_reciprocals line 52

    Source documentation

    The absolute constant is uniform in n. This is the divisor expansion needed when summing a rational phase with weight n/φ(n).

    theorem totient_ratio_le_divisor_reciprocals {n : ℕ} (hn : 0 < n) :
    (n:ℝ)/n.totient ≤ Real.exp 2 * ∑ d ∈ n.divisors, 1/(d:ℝ) := by
…