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 statement5 of 6

A construction of Cambie in the comments shows that $c\leq 1$ .

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

11 ∈ upperBounds Erdos1026.admissibleConstants

SolvedStatement only, no proof

Sources

Search problems.science