Erdős problem 254 · problems.science

If $A \subseteq \mathbb{N}$ has unbounded dyadic-shell counts and $\sum_{n \in A} \|\theta n\| = \infty$ for every $0 < \theta < 1$ , must $A$ be complete - is every sufficiently large integer a sum of distinct elements of $A$ ?

Sources

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

254.lean

Retained formal statement3 of 3

The hypothesis ¬ Summable (fun n : A ↦ distToNearestInt (θ * n)) used below says exactly that the partial sums of ‖θ n‖ over n ∈ A diverge, which is the form the linked proof uses. distToNearestInt is nonnegative, so this is an instance of not_summable_subtype_iff_tendsto_sum_indicator.

FormalConjectures/ErdosProblems/254.leanErdos254.not_summable_iff_tendsto_partial_sums4 linesExact file

1∀ (A : Set ℕ) (θ : ℝ),2  (¬Summable fun n => distToNearestInt (θ * ↑↑n)) ↔3    Filter.Tendsto (fun N => ∑ n ∈ Finset.range N, A.indicator (fun n => distToNearestInt (θ * ↑n)) n) Filter.atTop4      Filter.atTop

APIStatement only, no proof

Sources

Search problems.science