Erdős Problem 830

Reference: erdosproblems.com/830

structure Erdos830.IsAmicable (a b : ℕ) : Prop

We say that $a,b\in \mathbb{N}$ are an amicable pair if $\sigma(a)=\sigma(b)=a+b$.

• left : (ArithmeticFunction.sigma 1) a = a + b
• right : (ArithmeticFunction.sigma 1) b = a + b

theorem Erdos830.isAmicable_iff (a b : ℕ) : IsAmicable a b ↔ (ArithmeticFunction.sigma 1) a = a + b ∧ (ArithmeticFunction.sigma 1) b = a + b

@[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 = ↑(Finset.filter (fun (x : ℕ × ℕ) => match x with | (a, b) => a ≤ b ∧ Erdos830.IsAmicable a b) (Finset.Icc 1 ⌊x⌋₊ ×ˢ Finset.Icc 1 ⌊x⌋₊)).card

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

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 : (∃ (o : ℝ → ℝ), o =o[Filter.atTop] 1 ∧ ∀ᶠ (x : ℝ) in Filter.atTop, x ^ (1 - o x) < A x) ↔ sorry

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