Lemma 1 — pointwise minimization yields the least expected dual value
ProvedPooledRationing.AsymFeas.lemma_1Fix nonnegative weights and a deterministic policy that minimizes the Max-Weighted-Service objective over for every demand realization . Then
where is expected allocation cost minus weighted expected service, and is the corresponding pointwise minimum. This identifies a policy that attains the dual infimum.
Formalization Note The policy is measurable and feasible at every . Service measures are nonnegative and jointly measurable on the real extension of their original domain. One integrable envelope bounds service and absolute allocation cost on every feasible set, ensuring all expectations are genuine Bochner integrals. Randomized policies are finite mixtures when they occur elsewhere in this development.
import Mathlib import Definitions.Def_PooledRationing_AsymFeas_Setting
namespace PooledRationing.AsymFeas
open MeasureTheory
/-- Jiang–Wang–Zhang, Lemma 1, equation (17), p. 12. -/
theorem lemma_1 {n m : ℕ} (F : Measure (Fin n → ℝ)) [IsProbabilityMeasure F]
(P : (Fin m → ℝ) → (Fin n → ℝ) → Set (Sol n m)) (c : Fin m → ℝ)
(f : (Fin m → Fin n → ℝ) →ₗ[ℝ] ℝ)
(R : Fin n → ℝ → ℝ → ℝ) (β : Fin n → ℝ)
(hRnonneg : ∀ j s d, 0 ≤ R j s d)
(hRmeas : ∀ j, Measurable (fun p : ℝ × ℝ => R j p.1 p.2))
(h : (Fin n → ℝ) → ℝ) (hh : Integrable h F)
(hRenv : ∀ D, ∀ x ∈ P c D, ∀ j, R j (x.1 j) (D j) ≤ h D)
(hfenv : ∀ D, ∀ x ∈ P c D, |f x.2| ≤ h D)
(w : Fin n → ℝ) (hw : 0 ≤ w)
(φw : DetPolicy P c)
(hφw : ∀ D, IsMinOn (mwsObjective f R w D) (P c D) (φw.toFun D)) :
(⨅ φ : DetPolicy P c, Fdual F f R w φ) = Fdual F f R w φw ∧
Fdual F f R w φw = ∫ D, g P c f R w D ∂F := by sorry
end PooledRationing.AsymFeas
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.