Proof of Theorem 20, p. 21 — late dual coordinates

Proved

SecretaryAdvice.BinaryLimit.dual_closed_form_late

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

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

Let $n\ge1$ , $p,p'\in[1/2,1]$ , and let $t_N$ be the first positive $N$ coordinate of the rescaled greedy dual. For each $t_N\le i\le n$ ,

w_i^Y=p-\sum_{j=i}^{n-1}\frac{1-p'}j,\qquad w_i^N=1-p-\sum_{j=i}^{n-1}\frac{p'}j.

The formulas describe the late part of the dual exactly; an empty sum at $i=n$ is zero. When $p=1$ , $t_N=n+1$ , so this range is empty.

Formalization Note Times are 1-based natural numbers. The threshold is defined by positivity of the greedy coordinate.

Preamble

import Mathlib
import Definitions.Def_SecretaryAdvice_BinaryLimit_Dual

Formal statement

namespace SecretaryAdvice.BinaryLimit

theorem dual_closed_form_late (n : ℕ) (p pp : ℝ) (hn : 1 ≤ n) (hp0 : (1 / 2 : ℝ) ≤ p) (hp1 : p ≤ 1) (hpp0 : (1 / 2 : ℝ) ≤ pp) (hpp1 : pp ≤ 1)
    (i : ℕ) (hi : tN n p pp ≤ i) (hin : i ≤ n) :
    w n p pp i true = p - (∑ j ∈ Finset.Ico i n, (1 - pp) / (j : ℝ)) ∧
    w n p pp i false = (1 - p) - (∑ j ∈ Finset.Ico i n, pp / (j : ℝ)) := by sorry

end SecretaryAdvice.BinaryLimit

Source

Dütting et al., Secretaries with Advice, arXiv:2011.06726v1, p. 21, proof of Theorem 20, closed-form display

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