def value_function_feasible_set {E : Type u} [AddCommMonoid E] [Module ℝ E] {m p : ℕ} (X : Set E) (g : Fin m → E → EReal) (A : E →ₗ[ℝ] EuclideanSpace ℝ (Fin p)) (b : EuclideanSpace ℝ (Fin p)) (u : EuclideanSpace ℝ (Fin m)) (t : EuclideanSpace ℝ (Fin p)) : Set E

The feasible set for the perturbation parameter (u, t) consists of the points of X satisfying the coordinatewise inequality constraints g i x ≤ u i and the affine equality constraint A x + b = t.

@[simp]

theorem mem_value_function_feasible_set {E : Type u} [AddCommMonoid E] [Module ℝ E] {m p : ℕ} (X : Set E) (g : Fin m → E → EReal) (A : E →ₗ[ℝ] EuclideanSpace ℝ (Fin p)) (b : EuclideanSpace ℝ (Fin p)) (u : EuclideanSpace ℝ (Fin m)) (t : EuclideanSpace ℝ (Fin p)) (x : E) : x ∈ value_function_feasible_set X g A b u t ↔ x ∈ X ∧ (∀ (i : Fin m), g i x ≤ ↑(u.ofLp i)) ∧ A x + b = t

A point lies in the perturbation feasible set exactly when it belongs to X, satisfies every inequality constraint, and meets the affine equality constraint.

noncomputable def value_function {E : Type u} [AddCommMonoid E] [Module ℝ E] {m p : ℕ} (X : Set E) (f : E → EReal) (g : Fin m → E → EReal) (A : E →ₗ[ℝ] EuclideanSpace ℝ (Fin p)) (b : EuclideanSpace ℝ (Fin p)) : EuclideanSpace ℝ (Fin m) × EuclideanSpace ℝ (Fin p) → EReal

The perturbation value function assigns to (u, t) the infimum of f over the feasible set cut out by the perturbation constraints.

@[simp]

theorem value_function_apply {E : Type u} [AddCommMonoid E] [Module ℝ E] {m p : ℕ} (X : Set E) (f : E → EReal) (g : Fin m → E → EReal) (A : E →ₗ[ℝ] EuclideanSpace ℝ (Fin p)) (b : EuclideanSpace ℝ (Fin p)) (u : EuclideanSpace ℝ (Fin m)) (t : EuclideanSpace ℝ (Fin p)) : value_function X f g A b (u, t) = sInf (f '' value_function_feasible_set X g A b u t)

Evaluating the perturbation value function at (u, t) gives the infimum of f over the corresponding feasible set.

theorem value_function_feasible_set_mono_u {E : Type u} [AddCommMonoid E] [Module ℝ E] {m p : ℕ} (X : Set E) (g : Fin m → E → EReal) (A : E →ₗ[ℝ] EuclideanSpace ℝ (Fin p)) (b : EuclideanSpace ℝ (Fin p)) {u w : EuclideanSpace ℝ (Fin m)} {t : EuclideanSpace ℝ (Fin p)} (huw : ∀ (i : Fin m), u.ofLp i ≤ w.ofLp i) : value_function_feasible_set X g A b u t ⊆ value_function_feasible_set X g A b w t

Relaxing the inequality perturbation coordinates enlarges the perturbation feasible set.

theorem value_function_antitone_u {E : Type u} [AddCommMonoid E] [Module ℝ E] {m p : ℕ} (X : Set E) (f : E → EReal) (g : Fin m → E → EReal) (A : E →ₗ[ℝ] EuclideanSpace ℝ (Fin p)) (b : EuclideanSpace ℝ (Fin p)) {u w : EuclideanSpace ℝ (Fin m)} {t : EuclideanSpace ℝ (Fin p)} (huw : ∀ (i : Fin m), u.ofLp i ≤ w.ofLp i) : value_function X f g A b (u, t) ≥ value_function X f g A b (w, t)

For fixed equality perturbation t, the perturbation value function is antitone in the inequality perturbation parameter.

theorem nonempty_of_mem_effective_domain_value_function {E : Type u} [AddCommMonoid E] [Module ℝ E] {m p : ℕ} (X : Set E) (f : E → EReal) (g : Fin m → E → EReal) (A : E →ₗ[ℝ] EuclideanSpace ℝ (Fin p)) (b : EuclideanSpace ℝ (Fin p)) {u : EuclideanSpace ℝ (Fin m)} {t : EuclideanSpace ℝ (Fin p)} (huvt : (u, t) ∈ effective_domain (value_function X f g A b)) : X.Nonempty

Any effective-domain point of the perturbation value function forces the base set X to be nonempty.

theorem value_function_nonempty_of_proper {E : Type u} [AddCommMonoid E] [Module ℝ E] {m p : ℕ} (X : Set E) (f : E → EReal) (g : Fin m → E → EReal) (A : E →ₗ[ℝ] EuclideanSpace ℝ (Fin p)) (b : EuclideanSpace ℝ (Fin p)) (hv_proper : IsProperExtendedRealFunction (value_function X f g A b)) : X.Nonempty

Properness of the perturbation value function implies that the underlying constraint set X is nonempty.

@[implicit_reducible]

noncomputable def valueFunctionFeasibleSetMemDecidable {E : Type u} [AddCommMonoid E] [Module ℝ E] {m p : ℕ} (X : Set E) (g : Fin m → E → EReal) (A : E →ₗ[ℝ] EuclideanSpace ℝ (Fin p)) (b : EuclideanSpace ℝ (Fin p)) (u : EuclideanSpace ℝ (Fin m)) (t : EuclideanSpace ℝ (Fin p)) : DecidablePred fun (x : E) => x ∈ value_function_feasible_set X g A b u t

Helper for Lemma 3.4: membership in each perturbation feasible slice is classically decidable.

noncomputable def jointFeasibleObjective {E : Type u} [AddCommMonoid E] [Module ℝ E] {m p : ℕ} (X : Set E) (f : E → EReal) (g : Fin m → E → EReal) (A : E →ₗ[ℝ] EuclideanSpace ℝ (Fin p)) (b : EuclideanSpace ℝ (Fin p)) : (EuclideanSpace ℝ (Fin m) × EuclideanSpace ℝ (Fin p)) × E → EReal

Helper for Lemma 3.4: the joint feasible-if objective equals f x on feasible perturbation triples ((u, t), x) and ⊤ outside the perturbation feasible set.

theorem mem_jointFeasibleObjective_epigraph_iff {E : Type u} [AddCommMonoid E] [Module ℝ E] {m p : ℕ} (X : Set E) (f : E → EReal) (g : Fin m → E → EReal) (A : E →ₗ[ℝ] EuclideanSpace ℝ (Fin p)) (b : EuclideanSpace ℝ (Fin p)) (u : EuclideanSpace ℝ (Fin m)) (t : EuclideanSpace ℝ (Fin p)) (x : E) (r : ℝ) : jointFeasibleObjective X f g A b ((u, t), x) ≤ ↑r ↔ x ∈ value_function_feasible_set X g A b u t ∧ f x ≤ ↑r

Helper for Lemma 3.4: the real-epigraph condition for jointFeasibleObjective is exactly feasibility together with the epigraph condition for f.

theorem affineConstraint_combo_eq {E : Type u} [AddCommMonoid E] [Module ℝ E] {p : ℕ} (A : E →ₗ[ℝ] EuclideanSpace ℝ (Fin p)) (b : EuclideanSpace ℝ (Fin p)) {α β : ℝ} (hαβ : α + β = 1) {x₁ x₂ : E} {t₁ t₂ : EuclideanSpace ℝ (Fin p)} (hx₁ : A x₁ + b = t₁) (hx₂ : A x₂ + b = t₂) : A (α • x₁ + β • x₂) + b = α • t₁ + β • t₂

Helper for Lemma 3.4: affine equality constraints are preserved by convex combinations of feasible points and perturbations.

theorem combo_mem_valueFunctionFeasibleSet {E : Type u} [AddCommMonoid E] [Module ℝ E] {m p : ℕ} (X : Set E) (g : Fin m → E → EReal) (A : E →ₗ[ℝ] EuclideanSpace ℝ (Fin p)) (b : EuclideanSpace ℝ (Fin p)) (hg_convex : ∀ (i : Fin m), is_convex_function (g i)) (hX_convex : Convex ℝ X) {α β : ℝ} (hα : 0 ≤ α) (hβ : 0 ≤ β) (hαβ : α + β = 1) {u₁ u₂ : EuclideanSpace ℝ (Fin m)} {t₁ t₂ : EuclideanSpace ℝ (Fin p)} {x₁ x₂ : E} (hx₁ : x₁ ∈ value_function_feasible_set X g A b u₁ t₁) (hx₂ : x₂ ∈ value_function_feasible_set X g A b u₂ t₂) : α • x₁ + β • x₂ ∈ value_function_feasible_set X g A b (α • u₁ + β • u₂) (α • t₁ + β • t₂)

Helper for Lemma 3.4: the perturbation feasible set is closed under simultaneous convex combination of the primal point and perturbation parameters.

theorem jointFeasibleObjective_isConvex {E : Type u} [AddCommMonoid E] [Module ℝ E] {m p : ℕ} (X : Set E) (f : E → EReal) (g : Fin m → E → EReal) (A : E →ₗ[ℝ] EuclideanSpace ℝ (Fin p)) (b : EuclideanSpace ℝ (Fin p)) (hf_convex : is_convex_function f) (hg_convex : ∀ (i : Fin m), is_convex_function (g i)) (hX_convex : Convex ℝ X) : is_convex_function (jointFeasibleObjective X f g A b)

Helper for Lemma 3.4: the feasible-if joint objective on perturbationSpace × E is convex.

@[simp]

theorem valueFunction_eq_partialInf_jointFeasibleObjective {E : Type u} [AddCommMonoid E] [Module ℝ E] {m p : ℕ} (X : Set E) (f : E → EReal) (g : Fin m → E → EReal) (A : E →ₗ[ℝ] EuclideanSpace ℝ (Fin p)) (b : EuclideanSpace ℝ (Fin p)) (u : EuclideanSpace ℝ (Fin m)) (t : EuclideanSpace ℝ (Fin p)) : value_function X f g A b (u, t) = sInf (Set.range fun (x : E) => jointFeasibleObjective X f g A b ((u, t), x))

Helper for Lemma 3.4: the perturbation value function is the partial infimum of jointFeasibleObjective over the primal variable.

theorem value_function_is_convex {E : Type u} [AddCommMonoid E] [Module ℝ E] {m p : ℕ} (X : Set E) (f : E → EReal) (g : Fin m → E → EReal) (A : E →ₗ[ℝ] EuclideanSpace ℝ (Fin p)) (b : EuclideanSpace ℝ (Fin p)) (hf_convex : is_convex_function f) (hg_convex : ∀ (i : Fin m), is_convex_function (g i)) (hX_convex : Convex ℝ X) : is_convex_function (value_function X f g A b)

Lemma 3.4: if f and all constraint functions g i are convex and X is convex, then the perturbation value function is convex on ℝ^m × ℝ^p.