$-x\log x$ is maximized on $[0,1]$ exactly at $x=1/e$ , with value $1/e$

Proved

ClassicalSecretary.neg_mul_log_max

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

optimal-stoppingprobabilitysecretary-problem

Let $P(x) = -x\log x$ on $[0,1]$ , with $P(0)=0$ . Then:

$P(x) \le 1/e$ for every $x \in [0,1]$ ;
$P(1/e) = 1/e$ ;
if $P(x) = 1/e$ for some $x\in[0,1]$ , then $x = 1/e$ .

This identifies the limiting optimal cutoff fraction and the limiting optimal success probability.

Preamble

import Mathlib
import Definitions.Def_ClassicalSecretary_Model

open Finset Filter Topology

Formal statement

namespace ClassicalSecretary

theorem neg_mul_log_max :
    (∀ x ∈ Set.Icc (0 : ℝ) 1, -x * Real.log x ≤ Real.exp (-1)) ∧
    -Real.exp (-1) * Real.log (Real.exp (-1)) = Real.exp (-1) ∧
    (∀ x ∈ Set.Icc (0 : ℝ) 1, -x * Real.log x = Real.exp (-1) → x = Real.exp (-1)) := by sorry

end ClassicalSecretary

Source

Wikipedia, "Secretary problem", https://en.wikipedia.org/wiki/Secretary_problem, section "Deriving the optimal policy": "Taking the derivative of P(x) with respect to x, setting it to 0, and solving for x, we find that the optimal x is equal to 1/e".

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

−xlog⁡x-x\log x−xlogx is maximized on [0,1][0,1][0,1] exactly at x=1/ex=1/ex=1/e, with value 1/e1/e1/e

$-x\log x$ is maximized on $[0,1]$ exactly at $x=1/e$ , with value $1/e$