def setConstrainedParametricObjective {α : Type u} (f barf : α → ℝ) (t : ℝ) : α → ℝ

The pointwise max-type objective attached to f, barf, and the scalar parameter t, namely x ↦ max (f x - t) (barf x). This is the primitive owner object underlying the chapter's parametric value function.

@[simp]

theorem setConstrainedParametricObjective_apply {α : Type u} {f barf : α → ℝ} {t : ℝ} {x : α} : setConstrainedParametricObjective f barf t x = max (f x - t) (barf x)

Evaluating setConstrainedParametricObjective f barf t at x gives the defining pointwise maximum max (f x - t) (barf x).

noncomputable def parametricValueFunction {α : Type u} (Q : Set α) (f barf : α → ℝ) (t : ℝ) : EReal

The parametric value attached to the max-type model x ↦ max (f x - t) (barf x) is the extended-real optimal value of the corresponding constrained problem on Q.

theorem parametricValueFunction_eq_sInf_image {α : Type u} (Q : Set α) (f barf : α → ℝ) (t : ℝ) : parametricValueFunction Q f barf t = sInf ((fun (x : α) => ↑(setConstrainedParametricObjective f barf t x)) '' Q)

Unfolding parametricValueFunction gives the feasible-set image formula over Q.

theorem parametricValueFunction_def {α : Type u} (Q : Set α) (f barf : α → ℝ) (t : ℝ) : parametricValueFunction Q f barf t = sInf (Set.range fun (x : ↑Q) => ↑(setConstrainedParametricObjective f barf t ↑x))

Unfolding parametricValueFunction gives the displayed sInf formula over Q.

theorem setConstrainedParametricObjective_shift_le {α : Type u} (f barf : α → ℝ) (Δ t : ℝ) (hΔ : 0 ≤ Δ) (x : α) : setConstrainedParametricObjective f barf (t + Δ) x ≤ setConstrainedParametricObjective f barf t x

Increasing the parameter by a nonnegative amount can only decrease the pointwise max-type objective.

theorem setConstrainedParametricObjective_sub_le_shift {α : Type u} (f barf : α → ℝ) (Δ t : ℝ) (hΔ : 0 ≤ Δ) (x : α) : setConstrainedParametricObjective f barf t x - Δ ≤ setConstrainedParametricObjective f barf (t + Δ) x

Increasing the parameter by Δ ≥ 0 lowers the pointwise max-type objective by at most Δ.

theorem parametricValueFunction_sub_le_shift {α : Type u} (Q : Set α) (f barf : α → ℝ) (Δ t : ℝ) (hΔ : 0 ≤ Δ) : parametricValueFunction Q f barf t - ↑Δ ≤ parametricValueFunction Q f barf (t + Δ)

Lemma 3.3.6: for any model f and any Δ ≥ 0, shifting the parameter from t to t + Δ decreases the chapter parametric value by at most Δ. The textbook exact value f^*(t) and the approximate value \hat f_k^*(X; t) are the corresponding specializations of this owner theorem.

theorem parametricValueFunction_shift_le {α : Type u} (Q : Set α) (f barf : α → ℝ) (Δ t : ℝ) (hΔ : 0 ≤ Δ) : parametricValueFunction Q f barf (t + Δ) ≤ parametricValueFunction Q f barf t

For any model f and any Δ ≥ 0, shifting the parameter from t to t + Δ never increases the parametric value.

theorem parametricValueFunction_antitone {α : Type u} (Q : Set α) (f barf : α → ℝ) : Antitone (parametricValueFunction Q f barf)

The parametric value function is antitone in the scalar parameter. This is derived owner API: increasing t lowers the pointwise model x ↦ max (f x - t) (barf x), so the infimum over the fixed feasible set Q cannot increase.