Skip to content

Erdős problem 973

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

In [Er92f] (a different) Erdős refines this analysis, proving that if M2=min⁡zjmax⁡2≤k≤n+1∣∑1≤j≤nzjk∣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 zj∈Cz_j\in \mathbb{C} with max⁡∣zj∣=1\max \lvert z_j\rvert=1, then (1.746)−n<M2<(1.745)−n(1.746)^{-n} < M_2 < (1.745)^{-n}.

FormalConjectures/ErdosProblems/973.leanErdos973.erdos_973.variants.m2_bounds11 linesExact file
∀ n ≥ 2,  ∀ (M_2 : ℝ),    IsGLB        {M |          ∃ z,            (∀ j ∈ Finset.Icc 1 n, ‖z j‖ ≤ 1) ∧              (∃ j ∈ Finset.Icc 1 n, ‖z j‖ = 1) ∧                ∃ k ∈ Finset.Icc 2 (n + 1),                  M = ‖∑ j ∈ Finset.Icc 1 n, z j ^ k‖ ∧ ∀ m ∈ Finset.Icc 2 (n + 1), ‖∑ j ∈ Finset.Icc 1 n, z j ^ m‖ ≤ M}        M_2 →      1.746 ^ (-↑n) < M_2 ∧ M_2 < 1.745 ^ (-↑n)
SolvedStatement only, no proof