Average and divisibility of the divisor sum

TheoremA fixed positive integer divides the divisor sum of almost every natural number#●ready to prove

For a natural number \(l\) let \(\sigma(l)\) denote the sum of the positive divisors of \(l\), with \(\sigma(0) = 0\). Then for every positive integer \(N\), the set of natural numbers \(l\) such that \(N\) does not divide \(\sigma(l)\) has natural density \(0\).

theorem_wanted tendsto_density_not_dvd_sigma (N : ℕ)
    (hN : 1 ≤ N) :
    {l : ℕ | ¬ N ∣ ArithmeticFunction.sigma 1 l}.HasDensity 0

Sources

• Stoyan Dimitrov, "Generalizations of Amicable Numbers", Lemma 1.

Uses 1

Statement usesDensity of a set

TheoremLinear bound for the partial sums of the abundancy index#●ready to prove

For a positive integer \(n\) let \(\sigma(n)\) denote the sum of the positive divisors of \(n\), and let \(\zeta(2) = \sum_{n=1}^{\infty} 1/n^2\). Then for every real number \(x \ge 1\),

\[\sum_{n=1}^{\lfloor x \rfloor} \frac{\sigma(n)}{n} < \zeta(2)\, x.\]

theorem_wanted sum_sigma_div_lt (x : ℝ) (hx : 1 ≤ x) :
    ∑ n ∈ Finset.Icc 1 ⌊x⌋₊,
        (ArithmeticFunction.sigma 1 n : ℝ) / n <
      (∑' n : ℕ, (1 : ℝ) / (n + 1) ^ 2) * x

Sources

• Stoyan Dimitrov, "Generalizations of Amicable Numbers", Lemma 2.

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.