(7), p. 18 — 1 ≤ a ≤ 1/(1 − α) when p ≤ α < 1

Proved

EngagementOpt.Salad.eq_7

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

behavioral-economicsengagement-optimizationp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $\omega=(p,q,\bar v)\in\Omega$ and let $\alpha<1$ with $p\le\alpha$ . Then $a=\frac{1}{1-p}$ satisfies

1\ \le\ a\ \le\ \frac{1}{1-\alpha}.

In the proof of Theorem 4.2 this is applied to $a_S$ and $a_T$ , using condition 1 of the theorem.

Formalization Note The hypothesis $\alpha<1$ is implicit in the paper and is needed: for $\alpha=1$ , Lean's $1/0=0$ would make the upper bound false.

Preamble

import Mathlib
import Definitions.Def_EngagementOpt_Salad_Model

Formal statement

namespace EngagementOpt.Salad

/-- (7), p. 18: if `ω ∈ Ω`, `p ≤ α` and `α < 1`, then `1 ≤ a ≤ 1/(1 − α)`. -/
theorem eq_7 (ω : EngagementOpt.Misalign.Params) (hω : EngagementOpt.Misalign.InOmega ω) (α : ℝ) (hα : α < 1) (hp : ω.p ≤ α) :
    1 ≤ aCoef ω ∧ aCoef ω ≤ 1 / (1 - α) := by sorry

end EngagementOpt.Salad

Source

Kleinberg, Mullainathan, Raghavan, The Challenge of Understanding What Users Want, arXiv:2202.11776v3, p. 18, proof of Theorem 4.2, eq. (7)

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