Proposition 6, pp. 18–19 — under the W_it-policy, robust generation and ramping limits reduce to the extreme total-load scenarios
ProvedMultistageRUC.WitPolicy.proposition_6Consider the affine multistage robust unit commitment model under the -policy , with arbitrary output limits , ramp rates , commitments , initial state , and policy coefficients . Let be the budget uncertainty set (3), and let be trajectories whose total load is maximal, respectively minimal, over in every period ((19), (20)). Let and be the scenarios (21), (22).
Then for every generator and every period :
- the robust generation limits (8c) over are equivalent to the same constraints over the finite set ;
- the robust ramping-down limits (8d) at over are equivalent to the same constraints over , and so are the robust ramping-up limits (8e).
In symbols, for (8c),
This is Proposition 6 of the paper. It means that, under the -policy, the generation and ramping constraints can be imposed in advance through finitely many scenarios, so that only the worst-case cost constraint and the transmission constraints need constraint generation.
Formalization Note. The statement is for the -policy; the -policy (9) ("any simpler policy") is the instance . Lean periods are 0-based. At the first period the ramping constraints compare with the initial dispatch and use in place of . The commitments are arbitrary reals (the paper's restriction is not needed). The scenarios are hypotheses: any members of that maximize, respectively minimize, the total load of every period. The standing assumptions , of (3) are not needed once is assumed, and are omitted.
import Mathlib import Definitions.Def_MultistageRUC_WitPolicy_Setting
namespace MultistageRUC.WitPolicy
theorem proposition_6 {Ng Nd T : ℕ}
(pmin pmax : Fin Ng → ℝ) (RD RU SD SU : Fin Ng → Fin T → ℝ)
(x0 p0 : Fin Ng → ℝ) (x u v : Fin Ng → Fin T → ℝ) (w W : Fin Ng → Fin T → ℝ)
(dbar dhat : Fin T → Fin Nd → ℝ) (Γ : ℝ)
(dmax dmin : Fin T → Fin Nd → ℝ)
(hmax : IsMaxLoad (MultistageRUC.Equiv.uncSet dbar dhat Γ) dmax)
(hmin : IsMinLoad (MultistageRUC.Equiv.uncSet dbar dhat Γ) dmin) :
∀ i t,
(GenLimits pmin pmax x w W (MultistageRUC.Equiv.uncSet dbar dhat Γ) i t ↔
GenLimits pmin pmax x w W {dmin, dmax} i t) ∧
((RampDown RD SD x v p0 w W (MultistageRUC.Equiv.uncSet dbar dhat Γ) i t ↔
RampDown RD SD x v p0 w W {dmin, dmax, dminmax dmin dmax t, dmaxmin dmin dmax t} i t) ∧
(RampUp RU SU x0 x u p0 w W (MultistageRUC.Equiv.uncSet dbar dhat Γ) i t ↔
RampUp RU SU x0 x u p0 w W {dmin, dmax, dminmax dmin dmax t, dmaxmin dmin dmax t} i t)) := by sorry
end MultistageRUC.WitPolicy
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.