Skip to content

Problem

erdos:1026

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

Declared status
solved (Lean)
Formalization
formalized
OEIS
A391431 · A391490

Matching claims

0
No direct claims
This problem has no directly related claim record.