Erdős problem 1026 · problems.science

For a sequence of $n$ distinct reals, determine the largest constant $c$ such that some monotonic subsequence always has sum exceeding $(c-o(1))\cdot(1/\sqrt{n})$ times the total sum. Resolved as $c = 1$ .

Sources

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

7 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1026.lean

Retained formal statement6 of 6

Cambie makes the stronger conjecture that if $x_1,\ldots,x_{k^2}$ are distinct positive real numbers with $\sum x_i=1$ then there is always a monotonic subsequence with sum at least $1/k$ . This is a weighted-form of the Erdős-Szekeres theorem, and is also mentioned (as an open question) in a survey on the latter by Steele [St95].

This stronger conjecture appears to have been first proved by Tidor, Wang, and Yang [TWY16], and is also implicit in work of Wagner [Wa17]. A proof was given and formalised by Aristotle (see the comments), with an alternative proof provided by Chan.

FormalConjectures/ErdosProblems/1026.leanErdos1026.erdos_1026.variants.weighted_erdos_szekeres5 linesExact file

1∀ (k : ℕ),2  0 < k →3    ∀ (x : Fin (k ^ 2) → ℝ),4      Function.Injective x →5        (∀ (i : Fin (k ^ 2)), 0 < x i) → ∑ i, x i = 1 → ∃ S ∈ Erdos1026.monotonicSubsequenceSums x, 1 / ↑k ≤ S

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science