(11): the $t$ -derivative of (10) is $\bar v\,\varphi(\beta^t-1)-W$

Proved

EngagementOpt.Survey.eq_11

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

derivativeengagement-optimizationp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1real-analysis

Let $\beta>0$ with $\beta\ne1$ , $\bar v\ge0$ , $W>0$ , and extend the closed form (10) to real $s>0$ by

F(s)=\bar v\left(\frac{s\beta^s}{\beta^s-1}-\frac{1}{\beta-1}\right)-Ws .

Then for every real $t>0$ :

$F$ is differentiable at $t$ with

F'(t)=\bar v\,\varphi(\beta^t-1)-W,\qquad \varphi(x)=\frac{x+1}{x}\left(1-\frac{\ln(x+1)}{x}\right);

if $\bar v>0$ , then $F'(t)>0$ if and only if

\varphi(\beta^t-1)>\frac{W}{\bar v}.

With $x=\beta^t-1$ (so that $t\ln\beta=\ln(x+1)$ ), this is the criterion (11) for $\mathbb E[S\mid T=t]$ to be increasing in $t$ .

Formalization Note $\beta^s$ is the real power $\beta^s=e^{s\ln\beta}$ . On natural numbers it agrees with the natural-number power used in (10). The paper derives (11) in the case $q>p$ ( $\beta>1$ ) and reuses it for $q<p$ ; the identity is stated for every $\beta>0$ , $\beta\ne1$ .

Preamble

import Mathlib
import Definitions.Def_EngagementOpt_Survey_phi

Formal statement

namespace EngagementOpt.Survey

/-- arXiv:2202.11776v3, p. 21, the derivative computation ending in (11). Extend (10) to real
`s > 0` with `β ^ s = Real.rpow β s`. For `β > 0`, `β ≠ 1`, `v̄ ≥ 0`, `W > 0`, and real `t > 0`, the derivative of
`s ↦ v̄ (s β^s/(β^s - 1) - 1/(β - 1)) - W s` at `t` is `v̄ φ(β^t - 1) - W`, where
`φ(x) = (x + 1)/x · (1 - ln(x + 1)/x)`; and when `v̄ > 0` this derivative is positive exactly
when `φ(β^t - 1) > W/v̄`. -/
theorem eq_11 (β : ℝ) (hβ0 : 0 < β) (hβ1 : β ≠ 1) (v W t : ℝ)
    (hv : 0 ≤ v) (hW : 0 < W) (ht : 0 < t) :
    HasDerivAt (fun s : ℝ => v * (s * β ^ s / (β ^ s - 1) - 1 / (β - 1)) - W * s)
      (v * phi (β ^ t - 1) - W) t ∧
    (0 < v → (0 < v * phi (β ^ t - 1) - W ↔ W / v < phi (β ^ t - 1))) := by sorry

end EngagementOpt.Survey

Source

Kleinberg, Mullainathan, Raghavan, The Challenge of Understanding What Users Want, arXiv:2202.11776v3, p. 21, display chain ending in (11)

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

(11): the ttt-derivative of (10) is vˉ φ(βt−1)−W\bar v\,\varphi(\beta^t-1)-Wvˉφ(βt−1)−W

(11): the $t$ -derivative of (10) is $\bar v\,\varphi(\beta^t-1)-W$