Theorem 20, p. 20 — Y threshold precedes N threshold

Proved

SecretaryAdvice.BinaryLimit.thresholds_ordered

by mikedeng1 · Oct 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

binary-advicelinear-optimizationoptimal-stoppingp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1secretary-problem

For $n\ge1$ and $p,p'\in[1/2,1]$ , the first positive $Y$ coordinate of the rescaled greedy dual occurs no later than the first positive $N$ coordinate:

t_Y(n,p,p')\le t_N(n,p,p').

The order is the finite threshold relation asserted in Theorem 20. A value $n+1$ means that the corresponding signal is never accepted.

Preamble

import Mathlib
import Definitions.Def_SecretaryAdvice_BinaryLimit_Dual

Formal statement

namespace SecretaryAdvice.BinaryLimit

theorem thresholds_ordered (n : ℕ) (p pp : ℝ) (hn : 1 ≤ n) (hp0 : (1 / 2 : ℝ) ≤ p) (hp1 : p ≤ 1) (hpp0 : (1 / 2 : ℝ) ≤ pp) (hpp1 : pp ≤ 1) :
    tY n p pp ≤ tN n p pp := by sorry

end SecretaryAdvice.BinaryLimit

Source

Dütting et al., Secretaries with Advice, arXiv:2011.06726v1, p. 20, Theorem 20, first sentence

Human review

Endorsed by Shuze Chen · Oct 15, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 15, 2026
Confirmed by the mission captain (proposal self-audit).

View graph