Proof of Proposition 1 — the optimal expected value $V^\star$ is convex in $\mu$ on $[0,1]$

Proved

HumanMachine.Accuracy.vstar_convex

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

convexityp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1rational-inattention

Let $\lambda>0$ be the information cost. The DM's optimal expected value $V^\star(\mu)$ , as a function of her prior belief $\mu$ that the state is good, is convex on $[0,1]$ :

V^\star\big((1-t)\mu_1+t\mu_2\big)\le(1-t)V^\star(\mu_1)+tV^\star(\mu_2)\qquad\text{for all }\mu_1,\mu_2,t\in[0,1].

Together with Lemma 2 and Jensen's inequality this yields the value half of Proposition 1.

Preamble

import Mathlib
import Definitions.Def_HumanMachine_Accuracy_DecisionModel

Formal statement

namespace HumanMachine.Accuracy

/-- Proof of Proposition 1 (p. 33): for information cost `λ > 0`, the optimal expected value
`V⋆` is convex in the prior `μ` on `[0, 1]`. -/
theorem vstar_convex (lam : ℝ) (hlam : 0 < lam) :
    ConvexOn ℝ (Set.Icc (0 : ℝ) 1) (VStar lam) := by sorry

end HumanMachine.Accuracy

Source

Boyacı, Canyakmaz & de Véricourt, Human and Machine: The Impact of Machine Input on Decision-Making Under Cognitive Limitations, ESMT Working Paper 20-02 (Nov. 30, 2020), p. 33, Appendix A, proof of Proposition 1, second paragraph

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 Proposition 1 — the optimal expected value V⋆V^\starV⋆ is convex in μ\muμ on [0,1][0,1][0,1]

Proof of Proposition 1 — the optimal expected value $V^\star$ is convex in $\mu$ on $[0,1]$