Skip to content

Erdős problem 973

Does there exist a constant C>1C>1 such that, for every n2n\geq 2, there exists a sequence ziCz_i\in \mathbb{C} with z1=1z_1=1 and zi1\lvert z_i\rvert \geq 1 for all 1in1\leq i\leq n with max2kn+11inzik<Cn\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 statement1 of 4

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

This is Problem 7.3 in [Ha74], where it is attributed to Erdős.

FormalConjectures/ErdosProblems/973.leanErdos973.erdos_9736 linesExact file
TrueC > 1,n ≥ 2,z,        z 1 = 1 ∧          (∀ iFinset.Icc 1 n, 1 ≤ ‖z i‖) ∧ ∀ kFinset.Icc 2 (n + 1), ‖∑ iFinset.Icc 1 n, z i ^ k‖ < C ^ (-↑n)
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page