Erdős Problem 349

Reference: erdosproblems.com/349

def Erdos349.IsGoodPair (t α : ℝ) : Prop

This defines the core property of the problem: For what values of $t,\alpha \in (0,\infty)$ is the sequence $\lfloor t\alpha^n\rfloor$ complete?

Equations

• Erdos349.IsGoodPair t α = IsAddComplete (Set.range fun (n : ℕ) => ⌊t * α ^ n⌋)

theorem Erdos349.erdos_349 : {(t, α) : ℝ × ℝ | 0 < t ∧ 0 < α ∧ IsGoodPair t α} = sorry

For what values of $t,\alpha \in (0,\infty)$ is the sequence $\lfloor t\alpha^n\rfloor$ complete (that is, all sufficiently large integers are the sum of distinct integers of the form $\lfloor t\alpha^n\rfloor$)?

theorem Erdos349.complete_for_alpha_in_Ioo_one_to_goldenRatio (t α : ℝ) (ht : 0 < t) (hα : α ∈ Set.Ioo 1 ((1 + √5) / 2)) : IsGoodPair t α

It seems likely that the sequence is complete for all for all $t>0$ and all $1 < \alpha < \frac{1+\sqrt{5}}{2}$.

theorem Erdos349.exists_t_for_k_disjoint_segments (k : ℕ) : ∃ t ∈ Set.Ioo 0 1, ∃ (ι : Type), ↑k ≤ Set.univ.encard ∧ ∃ (I : ι → Set ℝ), (∀ (i : ι), 2 ≤ (I i).encard ∧ (I i).Nonempty ∧ IsConnected (I i)) ∧ Pairwise (Function.onFun Disjoint I) ∧ ⋃ (i : ι), I i ⊆ {α : ℝ | α > 0 ∧ IsGoodPair t α}

For any $k$ there exists some $t_k\in (0,1)$ such that the set of $\alpha$ such that the sequence $\lfloor t_k\alpha^n\rfloor$ is complete consists of at least $k$ disjoint line segments.

theorem Erdos349.erdos_349.variants.floor_3_halves_odd : {n : ℕ | Odd ⌊(3 / 2) ^ n⌋}.Infinite ↔ sorry

Is it true that the terms of the sequence $\lfloor (3/2)^n\rfloor$ are odd infinitely often and even infinitely often?

theorem Erdos349.erdos_349.variants.floor_3_halves_even : {n : ℕ | Even ⌊(3 / 2) ^ n⌋}.Infinite ↔ sorry

Is it true that the terms of the sequence $\lfloor (3/2)^n\rfloor$ are even infinitely often?