Part 2 of 2

TheoremGronwall's theorem#✓fully proved

Let \(\sigma(n)\) be the sum of the positive divisors of \(n\) and let \(\gamma\) be the Euler–Mascheroni constant. Then, as \(n\) runs over the natural numbers, \(\limsup_{n \to \infty} \sigma(n) / (n \log \log n) = e^{\gamma}\).

The quotient is read with the conventions \(\log 0 = 0\) and \(x/0 = 0\), so it is defined for every natural number \(n\); the finitely many \(n \le 2\) with \(n \log \log n \le 0\) do not affect the limit superior.

theorem gronwall_sigma_limsup :
    Filter.limsup
      (fun n : ℕ => ((ArithmeticFunction.sigma 1 n : ℕ) : ℝ) /
        ((n : ℝ) * Real.log (Real.log n))) Filter.atTop =
      Real.exp Real.eulerMascheroniConstant
Sources
  • S. Nazardonyavi and S. Yakubovich, "Extremely Abundant Numbers and the Riemann Hypothesis," Journal of Integer Sequences 17 (2014), Article 14.2.8, lines 98–111, https://cs.uwaterloo.ca/journals/JIS/VOL17/Nazar/nazar4.tex; original attribution: T. H. Gronwall, "Some asymptotic expressions in the theory of numbers," Transactions of the AMS 14 (1913), 113–122.

TheoremRelatively prime subset counts#✓fully proved

Let \(\ell < m\) and \(k \ge 1\) be natural numbers, and let \(\mu\) be the Möbius function. The number of nonempty subsets of \(\{\ell + 1, \dots, m\}\) whose elements have greatest common divisor \(1\) is

\[\sum_{d=1}^{m} \mu(d) \left(2^{\lfloor m/d \rfloor - \lfloor \ell/d \rfloor} - 1\right),\]

and the number of \(k\)-element subsets of \(\{\ell + 1, \dots, m\}\) whose elements have greatest common divisor \(1\) is

\[\sum_{d=1}^{m} \mu(d) \binom{\lfloor m/d \rfloor - \lfloor \ell/d \rfloor}{k}.\]
theorem mobius_formula_relatively_prime_subset_counts_interval
    (ℓ m k : ℕ) (h_lt : ℓ < m) (h_k : 1 ≤ k) :
    (((Finset.powerset (Finset.Ioc ℓ m)).filter
      (fun H => H.Nonempty ∧ Finset.gcd H id = 1)).card : ℤ) =
      ∑ d ∈ Finset.Icc 1 m,
        ArithmeticFunction.moebius d * ((2 : ℤ) ^ (m / d - ℓ / d) - 1) ∧
    (((Finset.powerset (Finset.Ioc ℓ m)).filter
      (fun H => H.card = k ∧ Finset.gcd H id = 1)).card : ℤ) =
      ∑ d ∈ Finset.Icc 1 m,
        ArithmeticFunction.moebius d * (Nat.choose (m / d - ℓ / d) k : ℤ)
Sources
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.