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 statement3 of 4

In [Er92f] (a different) Erdős refines this analysis, proving that if $M_2=\min_{z_j} \max_{2\leq k\leq n+1} \left\lvert \sum_{1\leq j\leq n}z_j^k\right\rvert$ where the minimum is taken over all $z_j\in \mathbb{C}$ with $\max \lvert z_j\rvert=1$ , then $(1.746)^{-n} < M_2 < (1.745)^{-n}$ .

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

1∀ n ≥ 2,2  ∀ (M_2 : ℝ),3    IsGLB4        {M |5          ∃ z,6            (∀ j ∈ Finset.Icc 1 n, ‖z j‖ ≤ 1) ∧7              (∃ j ∈ Finset.Icc 1 n, ‖z j‖ = 1) ∧8                ∃ k ∈ Finset.Icc 2 (n + 1),9                  M = ‖∑ j ∈ Finset.Icc 1 n, z j ^ k‖ ∧ ∀ m ∈ Finset.Icc 2 (n + 1), ‖∑ j ∈ Finset.Icc 1 n, z j ^ m‖ ≤ M}10        M_2 →11      1.746 ^ (-↑n) < M_2 ∧ M_2 < 1.745 ^ (-↑n)

SolvedStatement only, no proof

Sources

Search problems.science