(9) with $p=q$ : $\mathbb E[T_q\mid T_q+T_p=t+1]=\frac{t+1}{2}$

Proved

EngagementOpt.Survey.eq_9_p_eq_q

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

conditional-expectationengagement-optimizationgeometric-distributionp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $0<q<1$ and let $T_q,T_p$ be independent with the same law $\mathrm{Geom}(1-q)$ on $\{1,2,\dots\}$ (that is, $p=q$ ). Then for every session length $t\ge1$ ,

\mathbb E[T_q\mid T_q+T_p=t+1]=\frac{t+1}{2},

where the conditional mean is defined by (9).

When the two phases have the same law, every split of the session is equally likely, so the span is on average half of $t+1$ . This is the case $p=q$ of (10) and of Theorem 5.1(1).

Preamble

import Mathlib
import Definitions.Def_EngagementOpt_Survey_condMeanTq

Formal statement

namespace EngagementOpt.Survey

/-- arXiv:2202.11776v3, p. 20, (9) for `p = q`: if `p = q ∈ (0, 1)`, then
`E[T_q | T_q + T_p = t + 1] = (t + 1)/2` for every session length `t ≥ 1`. -/
theorem eq_9_p_eq_q (q : ℝ) (hq0 : 0 < q) (hq1 : q < 1) (t : ℕ) (ht : 1 ≤ t) :
    condMeanTq q q t = ((t : ℝ) + 1) / 2 := by sorry

end EngagementOpt.Survey

Source

Kleinberg, Mullainathan, Raghavan, The Challenge of Understanding What Users Want, arXiv:2202.11776v3, p. 20, sentence after (9)

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

(9) with p=qp=qp=q: E[Tq∣Tq+Tp=t+1]=t+12\mathbb E[T_q\mid T_q+T_p=t+1]=\frac{t+1}{2}E[Tq​∣Tq​+Tp​=t+1]=2t+1​

(9) with $p=q$ : $\mathbb E[T_q\mid T_q+T_p=t+1]=\frac{t+1}{2}$