Erdős problem 973 · problems.science

Does there exist a constant $C>1$ such that, for every $n\geq 2$ , there exists a sequence $z_i\in \mathbb{C}$ with $z_1=1$ and $\lvert z_i\rvert \geq 1$ for all $1\leq i\leq n$ with $\max_{2\leq k\leq n+1}\left\lvert \sum_{1\leq i\leq n}z_i^k\right\rvert < C^{-n}$ ?

Sources

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

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

973.lean

Retained formal statement4 of 4

Tang notes in the comments that Theorem 6.1 of [Tu84b] implies that, if $\lvert z_i\rvert \geq 1$ for all $i$ , then $\max_{2\leq k\leq n+1}\left\lvert \sum_{1\leq i\leq n}z_i^k\right\rvert \geq (2e)^{-(1+o(1))n}$ .

FormalConjectures/ErdosProblems/973.leanErdos973.erdos_973.variants.tang6 linesExact file

1∃ f,2  (f =o[Filter.atTop] fun x => 1) ∧3    ∀ᶠ (n : ℕ) in Filter.atTop,4      ∀ (z : ℕ → ℂ),5        (∀ i ∈ Finset.Icc 1 n, 1 ≤ ‖z i‖) →6          ∃ k ∈ Finset.Icc 2 (n + 1), ‖∑ i ∈ Finset.Icc 1 n, z i ^ k‖ ≥ (2 * Real.exp 1) ^ (-(1 + f n) * ↑n)

SolvedStatement only, no proof

Sources

Search problems.science