Erdős Problem 358

Reference: erdosproblems.com/358

def Erdos358.intervalRepresentations (A : ℕ → ℕ) (n : ℕ) : Set (ℕ × ℕ)

Equations

• Erdos358.intervalRepresentations A n = {(u, v) : ℕ × ℕ | n = ∑ i ∈ Finset.Icc u v, A i}

noncomputable def Erdos358.f (A : ℕ → ℕ) (n : ℕ) : ℕ

Equations

• Erdos358.f A n = Nat.card ↑(Erdos358.intervalRepresentations A n)

def Erdos358.intervalRepresentationsNonTrivial (A : ℕ → ℕ) (n : ℕ) : Set (ℕ × ℕ)

Equations

• Erdos358.intervalRepresentationsNonTrivial A n = {(u, v) : ℕ × ℕ | n = ∑ i ∈ Finset.Icc u v, A i ∧ u < v}

noncomputable def Erdos358.g (A : ℕ → ℕ) (n : ℕ) : ℕ

Equations

• Erdos358.g A n = Nat.card ↑(Erdos358.intervalRepresentationsNonTrivial A n)

theorem Erdos358.f_id : f id = fun (n : ℕ) => (Finset.filter Odd n.divisors).card

When $A_n = n$, the function $f$ defined above counts the number of odd divisors of $n$.

theorem Erdos358.erdos_358.parts.i : (∃ (A : ℕ → ℕ), StrictMono A ∧ Filter.Tendsto (f A) Filter.atTop Filter.atTop) ↔ sorry

Let $A=\{a_1 < \cdots\}$ be an infinite sequence of integers. Let $f(n)$ count the number of solutions to [n=\sum_{u\leq i\leq v}a_i.] Is there such an $A$ for which $f(n)\to \infty$ as $n\to \infty$?

theorem Erdos358.erdos_358.parts.ii : (∃ (A : ℕ → ℕ), StrictMono A ∧ ∀ᶠ (n : ℕ) in Filter.atTop, 2 ≤ f A n) ↔ sorry

Let $A=\{a_1 < \cdots\}$ be an infinite sequence of integers. Let $f(n)$ count the number of solutions to [n=\sum_{u\leq i\leq v}a_i.] Is there an $A$ such that $f(n)\geq 2$ for all large $n$?

theorem Erdos358.erdos_358.variants.prime_set : Filter.limsup (fun (n : ℕ) => ↑(f (Nat.nth Nat.Prime) n)) Filter.atTop = ⊤

When $A =\{a_1 < \cdots\}$ corresponds to the set of primes, it is conjectured that the $\limsup$ of the number of representations [n=\sum_{u\leq i\leq v}a_i] is infinite.

theorem Erdos358.erdos_358.variants.prime_set_density_representation : 0 < {n : ℕ | (intervalRepresentations (Nat.nth Nat.Prime) n).Nonempty}.upperDensity

When $A =\{a_1 < \cdots\}$ corresponds to the set of primes, it is conjectured that the set of numbers $n$ that have representations [n=\sum_{u\leq i\leq v}a_i] has positive upper density.

theorem Erdos358.erdos_358.variants.one_le : ∃ (A : ℕ → ℕ), StrictMono A ∧ ∀ᶠ (n : ℕ) in Filter.atTop, 1 ≤ g A n

It is conjectured that if $A =\{a_1 < \cdots\}$ and $g$ counts the number of representations [n=\sum_{u\leq i\leq v}a_i] such that the sum has at least two terms, then for all $n$ we have $1 \leq g(n)$ for sufficiently large $n$.