Skip to content

Erdős problem 973

Start work

Does there exist a constant C>1C>1 such that, for every n≥2n\geq 2, there exists a sequence zi∈Cz_i\in \mathbb{C} with z1=1z_1=1 and ∣zi∣≥1\lvert z_i\rvert \geq 1 for all 1≤i≤n1\leq i\leq n with max⁡2≤k≤n+1∣∑1≤i≤nzik∣<C−n\max_{2\leq k\leq n+1}\left\lvert \sum_{1\leq i\leq n}z_i^k\right\rvert < C^{-n}?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

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 ∣zi∣≥1\lvert z_i\rvert \geq 1 for all ii, then max⁡2≤k≤n+1∣∑1≤i≤nzik∣≥(2e)−(1+o(1))n\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
∃ f,  (f =o[Filter.atTop] fun x => 1) ∧    ∀ᶠ (n : ℕ) in Filter.atTop,      ∀ (z : ℕ → ℂ),        (∀ i ∈ Finset.Icc 1 n, 1 ≤ ‖z i‖) →          ∃ 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