Proof of Theorem 4.1, p. 16 — if $p_T\le p_S$ and $g_T(\omega_T)>g_T(\omega_S)$ , then $q_T>q_S$

Proved

EngagementOpt.Misalign.thm_4_1_step_q

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

behavioral-economicsengagementp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1recommender-systems

This is the first step of the proof of Theorem 4.1.

Let $\omega_S=(p_S,q_S,\bar v_S)$ and $\omega_T=(p_T,q_T,\bar v_T)$ be two points of $\Omega=[0,1)\times[0,1)\times\mathbb R_+$ , and let $g_T(\omega)=\frac1{1-q}+\frac{p}{1-p}$ . If

p_T\le p_S\qquad\text{and}\qquad g_T(\omega_T)>g_T(\omega_S),

then

q_T>q_S.

In words: if the engagement-maximizing content is not more moreish, its higher engagement must come from a longer span. No maximizer hypothesis is needed for this step.

Preamble

import Mathlib
import Definitions.Def_EngagementOpt_Misalign_Model

Formal statement

namespace EngagementOpt.Misalign

/-- Proof of Theorem 4.1, p. 16: for `ω_S, ω_T ∈ Ω`, if `p_T ≤ p_S` and
`g_T(ω_T) > g_T(ω_S)`, then `q_T > q_S`. -/
theorem thm_4_1_step_q (ωS ωT : Params) (hS : InOmega ωS) (hT : InOmega ωT)
    (hp : ωT.p ≤ ωS.p) (hgT : gT ωS < gT ωT) :
    ωS.q < ωT.q := by sorry

end EngagementOpt.Misalign

Source

Kleinberg, Mullainathan, Raghavan, The Challenge of Understanding What Users Want, arXiv:2202.11776v3, p. 16, proof of Theorem 4.1 (first display)

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

Proof of Theorem 4.1, p. 16 — if pT≤pSp_T\le p_SpT​≤pS​ and gT(ωT)>gT(ωS)g_T(\omega_T)>g_T(\omega_S)gT​(ωT​)>gT​(ωS​), then qT>qSq_T>q_SqT​>qS​

Proof of Theorem 4.1, p. 16 — if $p_T\le p_S$ and $g_T(\omega_T)>g_T(\omega_S)$ , then $q_T>q_S$