Lemma D.1: $\varphi(x)\ge\frac12$ for $x>0$ and $\varphi(x)\le\frac12$ for $-1<x<0$

Proved

EngagementOpt.Survey.lemma_D_1

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

inequalitieslogarithmp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1real-analysis

Let $\varphi(x)=\dfrac{x+1}{x}\left(1-\dfrac{\ln(x+1)}{x}\right)$ . Then

for every $x>0$ ,

\frac{x+1}{x}\left(1-\frac{\ln(x+1)}{x}\right)\ge\frac12;

for every $x$ with $-1<x<0$ ,

\frac{x+1}{x}\left(1-\frac{\ln(x+1)}{x}\right)\le\frac12 .

With $x=\beta^t-1$ , this compares the growth rate of $\mathbb E[T_q\mid T=t]$ with the rate $1/2$ of the symmetric case $p=q$ ; it gives parts 2(a) and 3(a) of Theorem 5.1.

Preamble

import Mathlib
import Definitions.Def_EngagementOpt_Survey_phi

Formal statement

namespace EngagementOpt.Survey

/-- arXiv:2202.11776v3, p. 40, Lemma D.1: `(x + 1)/x · (1 - ln(x + 1)/x) ≥ 1/2` for `x > 0`, and
`≤ 1/2` for `-1 < x < 0`. -/
theorem lemma_D_1 :
    (∀ x : ℝ, 0 < x → 1 / 2 ≤ phi x) ∧
    (∀ x : ℝ, -1 < x → x < 0 → phi x ≤ 1 / 2) := by sorry

end EngagementOpt.Survey

Source

Kleinberg, Mullainathan, Raghavan, The Challenge of Understanding What Users Want, arXiv:2202.11776v3, p. 40, Lemma D.1

Human review

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

View graph

Lemma D.1: φ(x)≥12\varphi(x)\ge\frac12φ(x)≥21​ for x>0x>0x>0 and φ(x)≤12\varphi(x)\le\frac12φ(x)≤21​ for −1<x<0-1<x<0−1<x<0

Lemma D.1: $\varphi(x)\ge\frac12$ for $x>0$ and $\varphi(x)\le\frac12$ for $-1<x<0$