Erdős problem 967 · problems.science

Let $1<a_1<\cdots$ be a sequence of integers such that $\sum\frac{1}{a_i}<\infty$ . Is it true that, for every $t\in \mathbb{R}$ , $1+\sum_{k}\frac{1}{a_k^{1+it}}\neq 0?$

Sources

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

5 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

967.lean

Retained formal statement3 of 5

Their interest in this problem arose from their proof that the statement that there are no such zeros is equivalent to the fact that, for any non-decreasing $f:\mathbb{R}\to \mathbb{R}_{\geq 0}$ which is bounded on every bounded interval and is $=0$ for $x<1$ , the relationship $f(x)+\sum_k f(x/a_k)=\left(1+\sum_k \frac{1}{a_k}+o(1)\right)x$ implies $f(x)=(1+o(1))x$ .

FormalConjectures/ErdosProblems/967.leanErdos967.erdos_967.variants.tauberian13 linesExact file

1∀ (a : ℕ → ℕ),2  StrictMono a →3    1 < a 0 →4      (Summable fun k => 1 / ↑(a k)) →5        ((∀ (t : ℝ), 1 + ∑' (k : ℕ), Erdos967.summand t (a k) ≠ 0) ↔6          ∀ (f : ℝ → ℝ),7            Monotone f →8              (∀ (x : ℝ), 0 ≤ f x) →9                (∀ x < 1, f x = 0) →10                  (∀ (x y : ℝ), BddAbove (f '' Set.Icc x y)) →11                    Filter.Tendsto (fun x => (f x + ∑' (k : ℕ), f (x / ↑(a k))) / x) Filter.atTop12                        (nhds (1 + ∑' (k : ℕ), 1 / ↑(a k))) →13                      Filter.Tendsto (fun x => f x / x) Filter.atTop (nhds 1))

SolvedStatement only, no proof

Sources

Search problems.science