Erdős Problem 830

Reference: erdosproblems.com/830

@[reducible, inline]

noncomputable abbrev Erdos830.A (x : ℝ) : ℝ

Let $A(x)$ counts the number of amicable $1\leq a\leq b\leq x$.

Equations

• Erdos830.A x = ↑{x ∈ Finset.Icc 1 ⌊x⌋₊ ×ˢ Finset.Icc 1 ⌊x⌋₊ | match x with | (a, b) => a ≤ b ∧ IsAmicable a b}.card

theorem Erdos830.erdos_830.parts.i : True ↔ {(a, b) : ℕ × ℕ | IsAmicable a b}.Infinite

Erdos Problem 830, Part 1 We say that $a,b\in \mathbb{N}$ are an amicable pair if $\sigma(a)=\sigma(b)=a+b$. Are there infinitely many amicable pairs?

theorem Erdos830.erdos_830.parts.ii : True ↔ ∃ (o : ℝ → ℝ), o =o[Filter.atTop] 1 ∧ ∀ᶠ (x : ℝ) in Filter.atTop, x ^ (1 - o x) < A x

Erdos Problem 830, Part 2 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 is it true that [A(x) > x^{1-o(1)}?]

theorem Erdos830.erdos_830.variants.erdos : A =o[Filter.atTop] id

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) = o(x)$.

theorem Erdos830.erdos_830.variants.pomerance : ∀ᶠ (x : ℝ) in Filter.atTop, A x ≤ x * Real.exp (-Real.nthRoot 3 (Real.log x))

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(-(\log x)^{1/3})$.

theorem Erdos830.erdos_830.variants.pomerance_stronger : ∃ (o : ℝ → ℝ), o =o[Filter.atTop] 1 ∧ ∀ᶠ (x : ℝ) in Filter.atTop, A x ≤ x * Real.exp (-(1 / 2 + o x) * √(Real.log x * Real.log (Real.log x)))

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})$.