(9) — the risk-neutral SF objective in closed form

Proved

MixFlex.RiskNeutral.sf_objective_eq

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

flexibilitynewsvendorp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1unreliable-supply

In the SF network of the mission's model, let $S=\tilde X_{N+1}=\tilde X_1+\dots+\tilde X_N$ be total demand, $c_{N+1}$ the flexible resource's marginal total cost and $K=K_{N+1}\ge 0$ the flexible investment. Then

V^{SF}_{RN}(K)=-(\lambda+(1-\lambda)\theta)\,c_{N+1}K+\theta p\Big(\mathbb E\big[S\,\mathbf 1\{S\le K\}\big]+K\big(1-\mathbb P(S\le K)\big)\Big).

This is equation (9) of the paper: the SF problem is a single-product newsvendor problem with Bernoulli investment failures, whose expected cost is the committed cost plus the delivered cost weighted by $\theta$ , and whose expected revenue is $\theta p\,\mathbb E[\min\{S,K\}]$ .

Formalization Note The paper writes $\int_0^{K}x f_{X_{N+1}}(x)\,dx$ ; since no density is assumed, it is rendered as $\mathbb E[S\,\mathbf 1\{S\le K\}]$ , which equals it for a nonnegative $S$ with a density.

Preamble

import Mathlib
import Definitions.Def_MixFlex_RiskNeutral_Model

Formal statement

namespace MixFlex.RiskNeutral

open MeasureTheory ProbabilityTheory

/-- (9), p. 41: the risk-neutral SF objective in closed form. The density integral
`∫_0^K x f(x) dx` is written as `E[S · 1{S ≤ K}]` with `S = X_1 + ⋯ + X_N`. -/
theorem sf_objective_eq (P : Params) (hP : P.Standing) {N : ℕ} {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) (X : Ω → Fin N → ℝ) (Y : Ω → Fin (N + 1) → ℝ) (hS : Setting P μ X Y)
    (cF K : ℝ) (hK : 0 ≤ K) :
    vSF P μ X Y cF K =
      -(P.lam + (1 - P.lam) * P.theta) * cF * K
        + P.theta * P.p * ((∫ ω, (∑ n, X ω n) * (if ∑ n, X ω n ≤ K then 1 else 0) ∂μ)
          + K * (1 - μ.real {ω | ∑ n, X ω n ≤ K})) := by sorry

end MixFlex.RiskNeutral

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. 41, §3.1, (9)

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