Totient of the sum of divisors
TheoremPollack–Pomerance sieve bound#●ready to prove
There is an absolute constant \(C > 0\) such that for every set \(P\) of primes and every real \(x > 1\), the number of integers \(n\) with \(1 \le n \le x\) that are divisible by no prime in \(P\) is at most \(C x \exp(-A_P(x))\), where \(A_P(x) = \sum_{p \in P,\ p \le x} 1/p\).
public theorem_wanted card_free_of_prime_set_le_exp_neg_sum_inv :
∃ C : ℝ, 0 < C ∧ ∀ (P : Set ℕ), (∀ p ∈ P, p.Prime) → ∀ x : ℝ, 1 < x →
((((Finset.Icc 1 ⌊x⌋₊).filter fun n => ∀ p ∈ P, ¬ p ∣ n).card : ℕ) : ℝ) ≤
C * x * Real.exp (-∑ p ∈ (Finset.Iic ⌊x⌋₊).filter (· ∈ P), (1 : ℝ) / p)Sources
- Anup B. Dixit and Saunak Bhattacharjee, On the Distribution of φ(σ(n)), INTEGERS 24 (2024), Article A65, Lemma 1, quoting Pollack and Pomerance, Lemma 3.
TheoremIntegers whose sum of divisors is not divisible by \(p\)#●ready to prove
There is an absolute constant \(C > 0\) such that for every prime \(p\) and every real \(x \ge e^p\), the number of integers \(n\) with \(1 \le n \le x\) for which \(p\) does not divide the sum of divisors \(\sigma(n)\) is at most \(C x (\log \log x / \log x)^{1/(p-1)}\).
public theorem_wanted card_not_dvd_sigma_le :
∃ C : ℝ, 0 < C ∧ ∀ p : ℕ, p.Prime → ∀ x : ℝ, Real.exp p ≤ x →
((((Finset.Icc 1 ⌊x⌋₊).filter fun n => ¬ p ∣ ArithmeticFunction.sigma 1 n).card : ℕ) :
ℝ) ≤
C * x * (Real.log (Real.log x) / Real.log x) ^ ((1 : ℝ) / ((p : ℝ) - 1))Sources
- Anup B. Dixit and Saunak Bhattacharjee, On the Distribution of φ(σ(n)), INTEGERS 24 (2024), Article A65, Lemma 3.
TheoremUpper bound for the number of \(n\) with \(\varphi(\sigma(n)) \ge c n\)#●ready to prove
Write \(\log_k\) for the \(k\)-fold iterated natural logarithm, so \(\log_3 x = \log \log \log x\), and let \(\varphi\) be Euler's totient function and \(\sigma\) the sum of divisors. For every real \(c > 0\) there is a constant \(C\) such that for all sufficiently large \(x\), the number of integers \(n\) with \(1 \le n \le x\) and \(\varphi(\sigma(n)) \ge c n\) is at most
The bound is only claimed for large \(x\) since it needs \(\log_4 x > 0\), that is, \(x > e^{e^e}\).
public theorem_wanted card_totient_sigma_ge_mul_le (c : ℝ) (hc : 0 < c) :
∃ C : ℝ, ∀ᶠ x in atTop,
((((Finset.Icc 1 ⌊x⌋₊).filter fun n : ℕ =>
c * n ≤ (Nat.totient (ArithmeticFunction.sigma 1 n) : ℝ)).card : ℕ) : ℝ) ≤
Real.pi ^ 2 * x / (6 * c * Real.log (Real.log (Real.log (Real.log x)))) +
C * (x * Real.log (Real.log (Real.log x)) /
(Real.log x ^ (1 / Real.log (Real.log (Real.log x))) *
Real.log (Real.log (Real.log (Real.log x)))))Sources
- Anup B. Dixit and Saunak Bhattacharjee, On the Distribution of φ(σ(n)), INTEGERS 24 (2024), Article A65, Theorem 1.
TheoremHow often \(\varphi(\sigma(n)) \ge n / f(n)\)#●ready to prove
Write \(\log_k\) for the \(k\)-fold iterated natural logarithm, so \(\log_3 x = \log \log \log x\), and let \(\varphi\) be Euler's totient function and \(\sigma\) the sum of divisors. Let \(f\) be a real function that is positive and non-decreasing on \((0, \infty)\) with \(f(x) = o(\log_4 x)\) as \(x \to \infty\), and let \(P_f(x)\) be the number of integers \(n\) with \(1 \le n \le x\) and \(\varphi(\sigma(n)) \ge n / f(n)\). Then, as \(x \to \infty\),
and \(P_f(x) = o(x)\).
public theorem_wanted card_totient_sigma_ge_div_isBigO (f : ℝ → ℝ)
(hpos : ∀ x, 0 < x → 0 < f x) (hmono : MonotoneOn f (Set.Ioi 0))
(hf : f =o[atTop] fun x => Real.log (Real.log (Real.log (Real.log x)))) :
((fun x : ℝ => ((((Finset.Icc 1 ⌊x⌋₊).filter fun n : ℕ =>
(n : ℝ) / f n ≤ (Nat.totient (ArithmeticFunction.sigma 1 n) : ℝ)).card : ℕ) : ℝ))
=O[atTop] fun x =>
x * f x / Real.log (Real.log (Real.log (Real.log x))) +
x * Real.log (Real.log (Real.log x)) /
(Real.log x ^ (1 / Real.log (Real.log (Real.log x))) *
Real.log (Real.log (Real.log (Real.log x))))) ∧
((fun x : ℝ => ((((Finset.Icc 1 ⌊x⌋₊).filter fun n : ℕ =>
(n : ℝ) / f n ≤ (Nat.totient (ArithmeticFunction.sigma 1 n) : ℝ)).card : ℕ) : ℝ))
=o[atTop] fun x => x)Sources
- Anup B. Dixit and Saunak Bhattacharjee, On the Distribution of φ(σ(n)), INTEGERS 24 (2024), Article A65, Theorem 2.
TheoremExceptions to \(\varphi(\sigma(n)) \le n / \log_5 n\)#●ready to prove
Write \(\log_k\) for the \(k\)-fold iterated natural logarithm, and let \(\varphi\) be Euler's totient function and \(\sigma\) the sum of divisors. The number of integers \(n\) with \(1 \le n \le x\) and \(\varphi(\sigma(n)) > n / \log_5 n\) is \(O(x \log_5 x / \log_4 x)\) as \(x \to \infty\).
The finitely many small \(n\) for which \(\log_5 n\) is not a positive real are absorbed by the \(O\)-term.
public theorem_wanted card_totient_sigma_gt_div_log_five_isBigO :
(fun x : ℝ => ((((Finset.Icc 1 ⌊x⌋₊).filter fun n : ℕ =>
(n : ℝ) / Real.log (Real.log (Real.log (Real.log (Real.log n)))) <
(Nat.totient (ArithmeticFunction.sigma 1 n) : ℝ)).card : ℕ) : ℝ))
=O[atTop] fun x =>
x * Real.log (Real.log (Real.log (Real.log (Real.log x)))) /
Real.log (Real.log (Real.log (Real.log x)))Sources
- Anup B. Dixit and Saunak Bhattacharjee, On the Distribution of φ(σ(n)), INTEGERS 24 (2024), Article A65, Corollary 1.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.