Proof of Proposition 4(i) — $E[u(w^{SD}(K))]\le E[u(w^{SF}(\sum_n K_n))]$ for every nondecreasing utility

Proved

MixFlex.Reliable.expectedUtility_le

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

expected-utilityflexibilitynewsvendorp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1stochastic-dominance

In the perfectly reliable SD/SF model with a common margin $p>0$ , common cost $c>0$ and nonnegative, measurable demand on a probability space, let $u:\mathbb R\to\mathbb R$ be any nondecreasing utility function (the class $U_1$ of §3.3) and let $K=(K_1,\dots,K_N)$ be a nonnegative dedicated investment. Then

E\big[u\big(w^{SD}(K)\big)\big]\le E\Big[u\Big(w^{SF}\Big(\sum_{n=1}^N K_n\Big)\Big)\Big].

Applied to an optimal SD investment, this shows that the SF network, at the same unit cost, can do at least as well as SD for every decision maker who prefers more wealth to less.

Formalization Note No integrability hypothesis is needed: for $K\ge 0$ and nonnegative demand both wealths lie almost surely in $[w_0-c\sum_nK_n,\;w_0+p\sum_nK_n]$ , and a monotone $u$ is measurable and bounded there, so both expectations are genuine Lebesgue integrals. No concavity, continuity or strict monotonicity of $u$ is assumed.

Preamble

import Mathlib
import Definitions.Def_MixFlex_Reliable_Model

open MeasureTheory

Formal statement

namespace MixFlex.Reliable
theorem expectedUtility_le (P : Params) (hP : P.Standing) {N : ℕ} {Ω : Type*}
    [MeasurableSpace Ω] (μ : Measure Ω) (X : Ω → Fin N → ℝ) (hS : Setting μ X)
    (u : ℝ → ℝ) (hu : Monotone u) (K : Fin N → ℝ) (hK : ∀ n, 0 ≤ K n) :
    expectedUtility μ u (wealthSD P X K) ≤
      expectedUtility μ u (wealthSF P X P.c (∑ n, K n)) := by sorry
end MixFlex.Reliable

Source

Tomlin and Wang, On the value of mix flexibility and dual sourcing in unreliable newsvendor networks, Manufacturing Service Oper. Management 7(1), 2005, p. 53, Appendix A, proof of PROPOSITION 4(i) (as quoted from Levy 1992, Equation (4)); p. 45, §3.3 (U_1)

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Proof of Proposition 4(i) — E[u(wSD(K))]≤E[u(wSF(∑nKn))]E[u(w^{SD}(K))]\le E[u(w^{SF}(\sum_n K_n))]E[u(wSD(K))]≤E[u(wSF(∑n​Kn​))] for every nondecreasing utility

Proof of Proposition 4(i) — $E[u(w^{SD}(K))]\le E[u(w^{SF}(\sum_n K_n))]$ for every nondecreasing utility