Erdős Problem 357

Reference: erdosproblems.com/357

def Erdos357.HasDistinctSums {ι : Type u_1} {α : Type u_2} [Preorder ι] [AddCommMonoid α] (a : ι → α) : Prop

Equations

• Erdos357.HasDistinctSums a = Set.InjOn (fun (J : Finset ι) => ∑ x ∈ J, a x) {J : Finset ι | J.OrdConnected}

noncomputable def Erdos357.f (n : ℕ) : ℕ

Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct.

Equations

• Erdos357.f n = sSup {k : ℕ | ∃ (a : Fin k → ℤ), Set.range a ⊆ Set.Icc 1 ↑n ∧ StrictMono a ∧ Erdos357.HasDistinctSums a}

theorem Erdos357.erdos_357.parts.i : (fun (n : ℕ) => ↑(f n)) =o[Filter.atTop] fun (n : ℕ) => ↑n

Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. Is $f(n)=o(n)$?

theorem Erdos357.erdos_357.parts.ii.bigO_version : sorry ≪ fun (n : ℕ) => ↑(f n)

Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. How does $f(n)$ grow? Can we find a (good) explicit function $g$ such that $g = O(f)$ ?

theorem Erdos357.erdos_357.parts.ii.bigO_version_symm : (fun (n : ℕ) => ↑(f n)) ≪ sorry

Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. How does $f(n)$ grow? Can we find a (good) explicit function $g$ such that $f = O(g)$ ?

theorem Erdos357.erdos_357.parts.ii.bigTheta_version : (fun (n : ℕ) => ↑(f n)) =Θ[Filter.atTop] sorry

Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. How does $f(n)$ grow? Can we find a (good) explicit function $g$ such that $f = \Theta(g)$ ?

theorem Erdos357.erdos_357.parts.ii.littleO_version : sorry =o[Filter.atTop] fun (n : ℕ) => ↑(f n)

Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. How does $f(n)$ grow? Can we find a (good) explicit function $g$ such that $g = o(f)$ ?

theorem Erdos357.erdos_357.parts.ii.littleO_version_symm : (fun (n : ℕ) => ↑(f n)) =o[Filter.atTop] sorry

Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. How does $f(n)$ grow? Can we find a (good) explicit function $g$ such that $f = o(g)$ ?

theorem Erdos357.erdos_357.variants.weisenberg : ∃ (o : ℕ → ℝ), o =o[Filter.atTop] 1 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, (2 + o n) * √↑n ≤ ↑(f n)

Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. It is known that $f(n) \geq (2+o(1))\sqrt{n}$. Source: See comment by Desmond Weisenberg here: https://www.erdosproblems.com/forum/thread/357.

theorem Erdos357.erdos_357.variants.infinite_set_lower_density (A : ℕ → ℕ) (hA : StrictMono A) : (∀ (I J : Finset ℕ), I.OrdConnected → J.OrdConnected → HasDistinctSums A) → (Set.range A).lowerDensity = 0

Suppose $A$ is an infinite set such that all finite sums of consecutive terms of $A$ are distinct. Then $A$ has lower density 0.

theorem Erdos357.erdos_357.variants.infinite_set_density (A : ℕ → ℕ) (hA : StrictMono A) : HasDistinctSums A → (Set.range A).HasDensity 0

Suppose $A$ is an infinite set such that all finite sums of consecutive terms of $A$ are distinct. Then it is conjectured that $A$ has density 0.

theorem Erdos357.erdos_357.variants.infinite_set_sum (A : ℕ → ℕ) (hA : StrictMono A) : HasDistinctSums A → Summable fun (i : ℕ) => 1 / ↑(A i)

Suppose $A$ is an infinite set such that all finite sums of consecutive terms of $A$ are distinct. Then it is conjectured that the sum $\sum_k \frac{1}{a_k}$ converges.

noncomputable def Erdos357.g (n : ℕ) : ℕ

Let $g(n)$ be the maximal $k$ such that there exist integers $1 \le a_1, \dotsc, a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct.

Equations

• Erdos357.g n = sSup {k : ℕ | ∃ (a : Fin k → ℕ), Set.range a ⊆ Set.Icc 1 n ∧ Erdos357.HasDistinctSums a}

theorem Erdos357.erdos_357.variants.hegyvari : ∃ (o : ℕ → ℝ) (o' : ℕ → ℝ), o =o[Filter.atTop] 1 ∧ o' =o[Filter.atTop] 1 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(g n) ∈ Set.Icc ((1 / 3 + o n) * ↑n) ((2 / 3 + o' n) * ↑n)

Let $g(n)$ be the maximal $k$ such that there exist integers $1 \le a_1, \dotsc, a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. It is known that $$\left(\frac 1 3 + o(1) \right)n \leq g(n) \leq \left(\frac 2 3 + o(1) \right)n.$$

noncomputable def Erdos357.h (n : ℕ) : ℕ

Let $h(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 \leq \dotsc \leq a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct.

Equations

• Erdos357.h n = sSup {k : ℕ | ∃ (a : Fin k → ℤ), Set.range a ⊆ Set.Icc 1 ↑n ∧ Monotone a ∧ Erdos357.HasDistinctSums a}

theorem Erdos357.erdos_357.variants.monotone.parts.i : (fun (n : ℕ) => ↑(h n)) =o[Filter.atTop] fun (n : ℕ) => ↑n

Let $h(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 \leq \dotsc \leq a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. Is $h(n)=o(n)$?

theorem Erdos357.erdos_357.variants.monotone.parts.ii.bigO_version : sorry ≪ fun (n : ℕ) => ↑(h n)

Let $h(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 \leq \dotsc \leq a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. How does $h(n)$ grow? Can we find a (good) explicit function $g$ such that $g = O(h)$ ?

theorem Erdos357.erdos_357.variants.monotone.parts.ii.bigO_version_symm : (fun (n : ℕ) => ↑(h n)) ≪ sorry

Let $h(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 \leq \dotsc \leq a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. How does $h(n)$ grow? Can we find a (good) explicit function $g$ such that $h = O(g)$ ?

theorem Erdos357.erdos_357.variants.monotone.parts.ii.bigTheta_version : (fun (n : ℕ) => ↑(h n)) =Θ[Filter.atTop] sorry

Let $h(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 \leq \dotsc \leq a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. How does $h(n)$ grow? Can we find a (good) explicit function $g$ such that $h = \Theta(g)$ ?

theorem Erdos357.erdos_357.variants.monotone.parts.ii.littleO_version : sorry =o[Filter.atTop] fun (n : ℕ) => ↑(h n)

Let $h(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 \leq \dotsc \leq a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. How does $h(n)$ grow? Can we find a (good) explicit function $g$ such that $g = o(h)$ ?

theorem Erdos357.erdos_357.variants.monotone.parts.ii.littleO_version_symm : (fun (n : ℕ) => ↑(h n)) =o[Filter.atTop] sorry

Let $h(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 \leq \dotsc \leq a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. How does $h(n)$ grow? Can we find a (good) explicit function $g$ such that $h = o(g)$ ?