Proposition 4 — with perfectly reliable resources, for every nondecreasing utility, the loss-averse and the CVaR objective
ProvedMixFlex.Reliable.flexibility_premium_nonneg_reliableConsider products with common margin , served either by dedicated resources of marginal cost (network SD) or by one flexible resource of marginal cost (network SF), all perfectly reliable. The firm has initial wealth , and the demand vector is nonnegative with an arbitrary joint distribution. Let and . Then for every flexible cost :
- for every nondecreasing utility (the class ), every nonnegative SD investment is matched by a nonnegative SF investment with
- the same holds for the loss-averse objective (6);
- for the CVaR objective (8), every pair with is matched by a pair with and a CVaR bracket at least as large.
In the paper's terms: the flexibility premium satisfies for all , and in particular for the loss-averse and the CVaR objective functions. Together with Proposition 1 (risk neutrality), this identifies when the intuition "flexibility is worth paying for" is valid: whenever supply is perfectly reliable, whatever the demand distribution and whatever the (monotone) risk attitude.
Formalization Note The flexibility premium of Definitions 1–2 is not defined as a number (the indifference cost need not be unique); "" is encoded as "SF is weakly preferred for every ", which is how p. 41 reads . "Weakly preferred" () is encoded without suprema, as the matching statements above. Perfect reliability () is built into the terminal wealths, which then no longer involve . Nonnegative, measurable demand and are stated explicitly; no density, independence or integrability of demand is assumed ("Let have any joint distribution").
import Mathlib import Definitions.Def_MixFlex_Reliable_Model open MeasureTheory
namespace MixFlex.Reliable
theorem flexibility_premium_nonneg_reliable (P : Params) (hP : P.Standing) {N : ℕ} {Ω : Type*}
[MeasurableSpace Ω] (μ : Measure Ω) (X : Ω → Fin N → ℝ) (hS : Setting μ X) :
(∀ u : ℝ → ℝ, Monotone u → PremiumNonneg P (SFPreferredEU P μ X u)) ∧
PremiumNonneg P (SFPreferredLA P μ X) ∧
PremiumNonneg P (SFPreferredCVaR P μ X) := by sorry
end MixFlex.Reliable
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.