Lemma 1, p. 494 — Π₂(q; a) is submodular in q
ProvedMitigateSupplyRisk.DualSourcing.lemma_1Consider the two-supplier random-capacity newsvendor: suppliers with design capacities , independent continuous capacity losses with laws , deliveries , and a demand with finite mean, independent of the losses. Let be the expected profit of the order vector at reliability indices .
Then is submodular on the quadrant : for all ,
where and are the componentwise maximum and minimum.
Submodularity says the two order quantities are substitutes: a larger order from one supplier lowers the marginal value of ordering from the other. The paper uses it to read off the direction of the optimal orders in the later results.
Formalization Note. The paper does not define "submodular"; the lattice inequality above is the standard definition, equivalent to for twice differentiable functions, and needs no differentiability. The statement holds for every nonnegative demand law with finite mean (no density is assumed).
import Mathlib import Definitions.Def_MitigateSupplyRisk_DualSourcing_Model open MeasureTheory ProbabilityTheory
namespace MitigateSupplyRisk.DualSourcing
/-- Lemma 1 (Wang, Gilland, Tomlin 2010, p. 494): the second-stage expected profit `Π₂(q; a)` is
submodular in the order vector `q` on the feasible quadrant `q ≥ 0`, in the lattice form
`Π₂(q ∨ q') + Π₂(q ∧ q') ≤ Π₂(q) + Π₂(q')` (componentwise max and min). Demand is any nonnegative
law with finite mean; no density is needed. -/
theorem lemma_1 (M : Model) (μ : Measure ℝ) [IsProbabilityMeasure μ]
(hμ0 : μ (Set.Iio 0) = 0) (hμint : Integrable id μ) (a : Fin 2 → ℝ)
(q q' : Fin 2 → ℝ) (hq : q ∈ Model.orders) (hq' : q' ∈ Model.orders) :
M.Pi2 μ (q ⊔ q') a + M.Pi2 μ (q ⊓ q') a ≤ M.Pi2 μ q a + M.Pi2 μ q' a := by sorry
end MitigateSupplyRisk.DualSourcing
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.