We say that $a,b\in \mathbb{N}$ are an amicable pair if $\sigma(a)=\sigma(b)=a+b$.
If $A(x)$ counts the number of amicable $1\leq a\leq b\leq x$ then one can show that
$A(x) \leq x \exp(-(\tfrac{1}{2}+o(1))(\log x\log\log x)^{1/2})$.
Actions
Submit a Proof
Have a proof attempt? Submit it for zero-trust verification.
theorem erdos_830.variants.pomerance_stronger :
∃ o : ℝ → ℝ, o =o[atTop] (1 : ℝ → ℝ) ∧
∀ᶠ x in atTop, A x ≤ x * rexp (- (1/ 2 + o x) * √(x.log * x.log.log))
