Euler's function and divisor sums along linear recurrences

TheoremLower bound for Euler's function and upper bound for the sum of divisors#●ready to prove

Let \(\varphi\) be Euler's totient function and \(\sigma(n)\) the sum of the positive divisors of \(n\). There is a constant \(C > 0\) such that \(\varphi(n)/n \ge C/\log\log n\) for every integer \(n \ge 3\), and there is a constant \(C'\) such that \(\sigma(n)/n \le C' \log\log n\) for every integer \(n \ge 3\).

public theorem_wanted totient_div_gg_and_sigma_div_ll_log_log :
    (∃ C : ℝ, 0 < C ∧ ∀ n : ℕ, 3 ≤ n →
        C / Real.log (Real.log n) ≤ (Nat.totient n : ℝ) / n) ∧
      ∃ C : ℝ, ∀ n : ℕ, 3 ≤ n →
        (ArithmeticFunction.sigma 1 n : ℝ) / n ≤ C * Real.log (Real.log n)

Sources

• Florian Luca and Makoko Campbell Manape, On the Euler Function of Linearly Recurrence Sequences, Fibonacci Quarterly 62 (2024), Article 62-4/luca09162024rev2, Lemma 1, quoted from Hardy and Wright, Theorems 323, 328 and 329.

TheoremSieve bound for integers without small prime factors#●ready to prove

Write \(p(n)\) for the least prime factor of an integer \(n \ge 2\), and set \(p(1) = 1\). There is a constant \(C\) such that for all real \(x\) and \(y\) with \(2 \le y \le x\), the number of integers \(1 \le n \le x\) with \(p(n) > y\) is at most \(C x / \log y\).

public theorem_wanted card_minFac_gt_le_div_log :
    ∃ C : ℝ, ∀ x y : ℝ, 2 ≤ y → y ≤ x →
      ((Finset.Icc 1 ⌊x⌋₊).filter (fun n => y < (Nat.minFac n : ℝ))).card ≤
        C * x / Real.log y

Sources

• Florian Luca and Makoko Campbell Manape, On the Euler Function of Linearly Recurrence Sequences, Fibonacci Quarterly 62 (2024), Article 62-4/luca09162024rev2, Lemma 2, quoted from Tenenbaum, page 397.

TheoremIntegers with many prime factors are rare#●ready to prove

Let \(\Omega(n)\) be the number of prime factors of \(n\) counted with multiplicity. There is a constant \(C\) such that for every real \(x \ge 10\), the number of integers \(1 \le n \le x\) with \(\Omega(n) \ge 10 \log\log x\) is at most \(C x / (\log x)^2\).

public theorem_wanted card_cardFactors_ge_ten_log_log_le :
    ∃ C : ℝ, ∀ x : ℝ, 10 ≤ x →
      ((Finset.Icc 1 ⌊x⌋₊).filter (fun n =>
          10 * Real.log (Real.log x) ≤ (ArithmeticFunction.cardFactors n : ℝ))).card ≤
        C * x / Real.log x ^ 2

Sources

• Florian Luca and Makoko Campbell Manape, On the Euler Function of Linearly Recurrence Sequences, Fibonacci Quarterly 62 (2024), Article 62-4/luca09162024rev2, Lemma 3.

TheoremIntegers whose sum of divisors has many divisors#●ready to prove

Let \(\sigma(n)\) be the sum of the positive divisors of \(n\) and \(\tau(m)\) the number of positive divisors of \(m\). There is a constant \(C\) such that for every real \(x \ge 10\), the number of integers \(1 \le n \le x\) with \(\tau(\sigma(n)) > \exp(\sqrt{\log x})\) is at most \(C x / (\log x)^2\).

public theorem_wanted card_divisors_sigma_gt_exp_sqrt_log_le :
    ∃ C : ℝ, ∀ x : ℝ, 10 ≤ x →
      ((Finset.Icc 1 ⌊x⌋₊).filter (fun n =>
          Real.exp (Real.sqrt (Real.log x)) <
            ((Nat.divisors (ArithmeticFunction.sigma 1 n)).card : ℝ))).card ≤
        C * x / Real.log x ^ 2

Sources

• Florian Luca and Makoko Campbell Manape, On the Euler Function of Linearly Recurrence Sequences, Fibonacci Quarterly 62 (2024), Article 62-4/luca09162024rev2, Lemma 4.

TheoremSchmidt's bound on the zeros of a linear recurrence#●ready to prove

Let \((U_n)_{n \ge 1}\) be a sequence of complex numbers satisfying \(U_{m+k} = c_0 U_m + c_1 U_{m+1} + \dots + c_{k-1} U_{m+k-1}\) for all \(m \ge 1\), with complex coefficients \(c_i\), where the order \(k\) of this recurrence is minimal among all linear recurrences with complex coefficients satisfied by \((U_n)_{n \ge 1}\), and \(k \ge 2\). Suppose the recurrence is nondegenerate: no root of its characteristic polynomial \(X^k - c_{k-1} X^{k-1} - \dots - c_0\) is \(0\), and no quotient of two distinct roots is a root of unity. Then \(U_n = 0\) for only finitely many \(n \ge 1\), and there are at most \(\exp(\exp(\exp(3k \log k)))\) such \(n\).

public theorem_wanted zero_set_card_le_exp_exp_exp (E : LinearRecurrence ℂ) (U : ℕ → ℂ)
    (hU : E.IsSolution (fun n => U (n + 1)))
    (hmin : ∀ E' : LinearRecurrence ℂ, E'.IsSolution (fun n => U (n + 1)) → E.order ≤ E'.order)
    (hnd : ∀ α β : ℂ, E.charPoly.IsRoot α → E.charPoly.IsRoot β →
      α ≠ 0 ∧ (α ≠ β → ∀ m : ℕ, 0 < m → (α / β) ^ m ≠ 1))
    (hk : 2 ≤ E.order) :
    {n : ℕ | 1 ≤ n ∧ U n = 0}.Finite ∧
      ({n : ℕ | 1 ≤ n ∧ U n = 0}.ncard : ℝ) ≤
        Real.exp (Real.exp (Real.exp (3 * E.order * Real.log E.order)))

Sources

• Florian Luca and Makoko Campbell Manape, On the Euler Function of Linearly Recurrence Sequences, Fibonacci Quarterly 62 (2024), Article 62-4/luca09162024rev2, Theorem 3, quoted from Schmidt.

TheoremFew small values of a nondegenerate integer linear recurrence#●ready to prove

Let \((U_n)_{n \ge 1}\) be a sequence of integers satisfying \(U_{m+k} = c_0 U_m + c_1 U_{m+1} + \dots + c_{k-1} U_{m+k-1}\) for all \(m \ge 1\), with integer coefficients \(c_i\), where the order \(k\) of this recurrence is minimal among all linear recurrences with integer coefficients satisfied by \((U_n)_{n \ge 1}\). Suppose the recurrence is nondegenerate: no complex root of its characteristic polynomial \(X^k - c_{k-1} X^{k-1} - \dots - c_0\) is \(0\), and no quotient of two distinct complex roots is a root of unity. Suppose also that the characteristic polynomial has at least two distinct complex roots, and let \(\alpha_1\) be a complex root of maximal modulus. Then there are a real \(c\) with \(0 < c < 1/3\) and real constants \(x_0\) and \(C\) such that for every real \(x \ge x_0\), the number of integers \(1 \le n \le x\) with \(|U_n| \le |\alpha_1|^{n(1 - x^{-c})}\) is at most \(C \sqrt{x}\).

public theorem_wanted card_abs_le_dominant_root_pow_le_sqrt (E : LinearRecurrence ℤ)
    (U : ℕ → ℤ) (hU : E.IsSolution (fun n => U (n + 1)))
    (hmin : ∀ E' : LinearRecurrence ℤ, E'.IsSolution (fun n => U (n + 1)) → E.order ≤ E'.order)
    (hnd : ∀ α β : ℂ, (E.charPoly.map (Int.castRingHom ℂ)).IsRoot α →
      (E.charPoly.map (Int.castRingHom ℂ)).IsRoot β →
      α ≠ 0 ∧ (α ≠ β → ∀ m : ℕ, 0 < m → (α / β) ^ m ≠ 1))
    (hs : ∃ α β : ℂ, (E.charPoly.map (Int.castRingHom ℂ)).IsRoot α ∧
      (E.charPoly.map (Int.castRingHom ℂ)).IsRoot β ∧ α ≠ β)
    (α₁ : ℂ) (hα₁ : (E.charPoly.map (Int.castRingHom ℂ)).IsRoot α₁)
    (hmax : ∀ β : ℂ, (E.charPoly.map (Int.castRingHom ℂ)).IsRoot β → ‖β‖ ≤ ‖α₁‖) :
    ∃ c : ℝ, 0 < c ∧ c < 1 / 3 ∧ ∃ x₀ C : ℝ, ∀ x : ℝ, x₀ ≤ x →
      ((Finset.Icc 1 ⌊x⌋₊).filter (fun n =>
          (|U n| : ℝ) ≤ ‖α₁‖ ^ ((n : ℝ) * (1 - x ^ (-c))))).card ≤ C * Real.sqrt x

Sources

• Florian Luca and Makoko Campbell Manape, On the Euler Function of Linearly Recurrence Sequences, Fibonacci Quarterly 62 (2024), Article 62-4/luca09162024rev2, Lemma 5.

TheoremEuler's function and the sum of divisors along a linear recurrence#●ready to prove

Let \((U_n)_{n \ge 1}\) be a sequence of integers satisfying \(U_{m+k} = c_0 U_m + c_1 U_{m+1} + \dots + c_{k-1} U_{m+k-1}\) for all \(m \ge 1\), with integer coefficients \(c_i\), where the order \(k\) of this recurrence is minimal among all linear recurrences with integer coefficients satisfied by \((U_n)_{n \ge 1}\). Suppose the recurrence is nondegenerate: no complex root of its characteristic polynomial \(X^k - c_{k-1} X^{k-1} - \dots - c_0\) is \(0\), and no quotient of two distinct complex roots is a root of unity. Suppose also that there is no polynomial \(P\) with rational coefficients such that \(|U_n| = P(n)\) for all sufficiently large \(n\). Let \(\varphi\) be Euler's totient function and \(\sigma(m)\) the sum of the positive divisors of \(m\), with \(\varphi(0) = \sigma(0) = 0\). Then there are real constants \(x_0\) and \(C\) such that for every real \(x \ge x_0\), the number of integers \(1 \le n \le x\) with \(\varphi(|U_n|) < |U_{\varphi(n)}|\) is at most \(C x / \log x\), and the number of integers \(1 \le n \le x\) with \(|U_{\sigma(n)}| < \sigma(|U_n|)\) is at most \(C x / \log x\).

MetaMathlibExt.card_totient_sigma_inequality_fails_le_div_log · 15 lines

public theorem_wanted card_totient_sigma_inequality_fails_le_div_log (E : LinearRecurrence ℤ)
    (U : ℕ → ℤ) (hU : E.IsSolution (fun n => U (n + 1)))
    (hmin : ∀ E' : LinearRecurrence ℤ, E'.IsSolution (fun n => U (n + 1)) → E.order ≤ E'.order)
    (hnd : ∀ α β : ℂ, (E.charPoly.map (Int.castRingHom ℂ)).IsRoot α →
      (E.charPoly.map (Int.castRingHom ℂ)).IsRoot β →
      α ≠ 0 ∧ (α ≠ β → ∀ m : ℕ, 0 < m → (α / β) ^ m ≠ 1))
    (hpoly : ¬ ∃ P : Polynomial ℚ, ∀ᶠ n in atTop, ((|U n| : ℤ) : ℚ) = P.eval (n : ℚ)) :
    ∃ x₀ C : ℝ, ∀ x : ℝ, x₀ ≤ x →
      ((Finset.Icc 1 ⌊x⌋₊).filter (fun n =>
          ((Nat.totient (U n).natAbs : ℕ) : ℤ) < |U (Nat.totient n)|)).card ≤
          C * x / Real.log x ∧
        ((Finset.Icc 1 ⌊x⌋₊).filter (fun n =>
          |U (ArithmeticFunction.sigma 1 n)| <
            ((ArithmeticFunction.sigma 1 (U n).natAbs : ℕ) : ℤ))).card ≤
          C * x / Real.log x

Sources

• Florian Luca and Makoko Campbell Manape, On the Euler Function of Linearly Recurrence Sequences, Fibonacci Quarterly 62 (2024), Article 62-4/luca09162024rev2, Theorem 1.

7 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.