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

Hanani [Ha57] showed that every sequence is the disjoint union of at most $(\sqrt{2}+o(1))\sqrt{n}$ many monotonic subsequences.

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

1∀ (ε : ℝ),2  0 < ε →3    ∀ᶠ (n : ℕ) in Filter.atTop,4      ∀ (x : Fin n → ℝ),5        Function.Injective x →6          ∃ m I,7            (∀ (j : Fin m), MonotoneOn x ↑(I j) ∨ AntitoneOn x ↑(I j)) ∧8              (Pairwise fun j k => Disjoint (I j) (I k)) ∧ Finset.univ.biUnion I = Finset.univ ∧ ↑m ≤ (√2 + ε) * √↑n

SolvedStatement only, no proof

Sources

Search problems.science