Prove2Me

Proof of Proposition 4(i) — FWSF≤FWSDF_{W^{SF}}\le F_{W^{SD}}: the pooled SF wealth first-order dominates the SD wealth

Proved
MixFlex.Reliable.sf_cdf_le_sd_cdf

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

flexibilitynewsvendorp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1stochastic-dominance

In the perfectly reliable SD/SF model with nonnegative, measurable demand on a probability space, let K=(K1,…,KN)K=(K_1,\dots,K_N) be a dedicated investment and let the flexible network invest ∑nKn\sum_n K_n at the common cost cc. Then for every level w∈Rw\in\mathbb R,

P(wSF(∑n=1NKn)≤w)≤P(wSD(K)≤w),\mathbb P\Big(w^{SF}\Big(\sum_{n=1}^N K_n\Big)\le w\Big)\le\mathbb P\big(w^{SD}(K)\le w\big),

that is, the distribution function of the SF wealth lies below that of the SD wealth, and the SF wealth first-order stochastically dominates the SD wealth.

This is the step of the proof of Proposition 4 from which the expected-utility and CVaR comparisons follow.

Formalization Note The page states the inequality for the profits W~=W−w0\tilde W=W-w_0; shifting both by the same constant w0w_0 does not change it, so it is stated for terminal wealth.

Preamble
import Mathlib
import Definitions.Def_MixFlex_Reliable_Model

open MeasureTheory
Formal statement
namespace MixFlex.Reliable
theorem sf_cdf_le_sd_cdf (P : Params) (hP : P.Standing) {N : ℕ} {Ω : Type*}
    [MeasurableSpace Ω] (μ : Measure Ω) (X : Ω → Fin N → ℝ) (hS : Setting μ X)
    (K : Fin N → ℝ) (w : ℝ) :
    μ.real {ω | wealthSF P X P.c (∑ n, K n) ω ≤ w} ≤ μ.real {ω | wealthSD P X K ω ≤ w} := 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), after (A-6)
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