Erdős problem 1026

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

The source's own material, retained exactly.

7 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1026.lean

Retained formal statement2 of 6

In particular, this shows that $c=1$ .

FormalConjectures/ErdosProblems/1026.leanErdos1026.erdos_1026.variants.eq_one1 lineExact file

1IsGreatest Erdos1026.admissibleConstants 1

SolvedStatement only, no proof