def
extendedFeasibleSet
{Q : Type u}
{ι : Type v}
{α : Type w}
[Preorder α]
(constraints : ι → Q → α)
(ε : α)
:
Set Q
Definition 3.43: for a domain Q, a family of constraint functions fⱼ : Q → α, and a
threshold ε : α, the extended feasible set consists of the points x : Q such that every
constraint value satisfies fⱼ(x) ≤ ε. Its Lean surface notation is 𝓕[constraints](ε).
Instances For
@[simp]
theorem
mem_extendedFeasibleSet_iff
{Q : Type u}
{ι : Type v}
{α : Type w}
[Preorder α]
(constraints : ι → Q → α)
(ε : α)
{x : Q}
:
x ∈ extendedFeasibleSet constraints ε ↔ ∀ (j : ι), constraints j x ≤ ε
Membership in the extended feasible set at tolerance ε is exactly the coordinatewise
inequality family fⱼ(x) ≤ ε.
theorem
extendedFeasibleSet_eq_inequalityConstrainedFeasibleSet
{Q : Type u}
{m : ℕ}
(constraints : Fin m → Q → ℝ)
(ε : ℝ)
:
extendedFeasibleSet constraints ε = inequalityConstrainedFeasibleSet Set.univ fun (j : Fin m) (x : Q) => constraints j x - ε
For finite real-valued constraints, the source-facing extended feasible set is exactly the
Chapter 3 feasible-set owner applied to the shifted family x ↦ fⱼ(x) - ε on Set.univ.