Integral approximation: $P_n(r_n) \to -x\log x$ when $r_n/n \to x$

Proved

ClassicalSecretary.tendsto_successProb_cutoffRule

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

optimal-stoppingprobabilitysecretary-problem

Let $(r_n)$ be cutoffs with $1 \le r_n \le n$ for all large $n$ , and suppose $r_n/n \to x$ for some $x \in [0,1]$ . Then

\lim_{n\to\infty} P_n(\text{cutoff } r_n) = x\int_x^1\frac{dt}{t} = -x\log x,

where the right-hand side is read as $0$ at $x = 0$ .

This is the passage from the exact finite formula to its continuous limit.

Formalization Note The limit is written as -x * Real.log x. Since Real.log 0 = 0, this equals $0$ at $x=0$ , which is the correct limit there.

Preamble

import Mathlib
import Definitions.Def_ClassicalSecretary_Model

open Finset Filter Topology

Formal statement

namespace ClassicalSecretary

theorem tendsto_successProb_cutoffRule (r : ℕ → ℕ) (x : ℝ) (hx : x ∈ Set.Icc (0 : ℝ) 1)
    (hr : ∀ᶠ n in atTop, 1 ≤ r n ∧ r n ≤ n)
    (hlim : Tendsto (fun n : ℕ => (r n : ℝ) / (n : ℝ)) atTop (𝓝 x)) :
    Tendsto (fun n : ℕ => successProb n (cutoffRule (r n))) atTop
      (𝓝 (-x * Real.log x)) := by sorry

end ClassicalSecretary

Source

Wikipedia, "Secretary problem", https://en.wikipedia.org/wiki/Secretary_problem, section "Deriving the optimal policy", paragraph "Letting n tend to infinity, writing x as the limit of (r−1)/n ... the sum can be approximated by the integral P(x) = x∫_x^1 (1/t) dt = −x ln(x)".

Human review

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

View graph

Integral approximation: Pn(rn)→−xlog⁡xP_n(r_n) \to -x\log xPn​(rn​)→−xlogx when rn/n→xr_n/n \to xrn​/n→x

Integral approximation: $P_n(r_n) \to -x\log x$ when $r_n/n \to x$