Prove2Me

(A-4)–(A-6) — pooling all dedicated capacity into the flexible resource never lowers terminal wealth

Proved
MixFlex.Reliable.wealth_gap_nonneg

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

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

Consider the SD and SF networks with perfectly reliable resources, a common margin p>0p>0 and a common marginal cost cc for every resource, the flexible one included. Take any dedicated investment K=(K1,…,KN)K=(K_1,\dots,K_N) and let the flexible network invest the total KN+1=∑nKnK_{N+1}=\sum_{n}K_n. For every demand realization x=(x1,…,xN)x=(x_1,\dots,x_N) the terminal wealths (A-4)–(A-5) satisfy

wSF(∑n=1NKn)−wSD(K)=p(min⁡{∑n=1Nxn,∑n=1NKn}−∑n=1Nmin⁡{xn,Kn})≥0.w^{SF}\Big(\sum_{n=1}^N K_n\Big)-w^{SD}(K)=p\Big(\min\Big\{\sum_{n=1}^N x_n,\sum_{n=1}^N K_n\Big\}-\sum_{n=1}^N\min\{x_n,K_n\}\Big)\ge 0 .

This pathwise comparison is the whole content of the paper's proof of Proposition 4: every later step compares distributions or objectives derived from it.

Formalization Note The statement is pointwise in the sample point and needs no sign condition on KK or on demand; the inequality min⁡{∑xn,∑Kn}≥∑min⁡{xn,Kn}\min\{\sum x_n,\sum K_n\}\ge\sum\min\{x_n,K_n\} holds for all reals.

Preamble
import Mathlib
import Definitions.Def_MixFlex_Reliable_Model
Formal statement
namespace MixFlex.Reliable
theorem wealth_gap_nonneg (P : Params) (hP : P.Standing) {N : ℕ} {Ω : Type*}
    (X : Ω → Fin N → ℝ) (K : Fin N → ℝ) (ω : Ω) :
    wealthSF P X P.c (∑ n, K n) ω - wealthSD P X K ω =
        P.p * (min (∑ n, X ω n) (∑ n, K n) - ∑ n, min (X ω n) (K n)) ∧
      0 ≤ wealthSF P X P.c (∑ n, K n) ω - wealthSD P X K ω := 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, pp. 52–53, Appendix A, proof of PROPOSITION 4(i), (A-4)–(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