noncomputable def saddlePointObjective {E : Type u} {E₁ : Type v} {P : Set E} {Ω : Set E₁} (Ψ₀ : ↑Ω → ↑P → ℝ) : ↑P → EReal

Definition 7.63 (1): for a saddle-function model Ψ₀ : Ω × P → ℝ, the associated primal objective is the lower value ψ(x) = inf_{u ∈ Ω} Ψ₀(u, x), formalized through the canonical infimal-projection owner on EReal so empty or unbounded-below slices are represented faithfully.

theorem saddlePointObjective_def {E : Type u} {E₁ : Type v} {P : Set E} {Ω : Set E₁} (Ψ₀ : ↑Ω → ↑P → ℝ) : saddlePointObjective Ψ₀ = partialInfProjection Set.univ fun (z : ↑P × ↑Ω) => ↑(Ψ₀ z.2 z.1)

Expanding saddlePointObjective identifies it with the chapter's canonical infimal-projection owner on the unconstrained product domain P × Ω.

@[simp]

theorem saddlePointObjective_apply {E : Type u} {E₁ : Type v} {P : Set E} {Ω : Set E₁} (Ψ₀ : ↑Ω → ↑P → ℝ) (x : ↑P) : saddlePointObjective Ψ₀ x = sInf (Set.range fun (u : ↑Ω) => ↑(Ψ₀ u x))

Evaluating saddlePointObjective Ψ₀ at x gives the infimum of the u-slice of Ψ₀ over Ω, viewed in EReal.

noncomputable def saddlePointDualFunction {E : Type u} {E₁ : Type v} {P : Set E} {Ω : Set E₁} (Ψ₀ : ↑Ω → ↑P → ℝ) : ↑Ω → EReal

Definition 7.63 (2): for a saddle-function model Ψ₀ : Ω × P → ℝ, the associated dual function is the upper value ψ⋆(u) = sup_{x ∈ P} Ψ₀(u, x), formalized through the Chapter 7 maximal-value owner on EReal so empty or unbounded-above slices are represented faithfully.

theorem saddlePointDualFunction_def {E : Type u} {E₁ : Type v} {P : Set E} {Ω : Set E₁} (Ψ₀ : ↑Ω → ↑P → ℝ) : saddlePointDualFunction Ψ₀ = fun (u : ↑Ω) => maximalValueOn Set.univ (Ψ₀ u)

Expanding saddlePointDualFunction identifies it with the chapter's canonical maximal-value owner applied to each primal slice of the saddle map.

@[simp]

theorem saddlePointDualFunction_apply {E : Type u} {E₁ : Type v} {P : Set E} {Ω : Set E₁} (Ψ₀ : ↑Ω → ↑P → ℝ) (u : ↑Ω) : saddlePointDualFunction Ψ₀ u = sSup (Set.range fun (x : ↑P) => ↑(Ψ₀ u x))

Evaluating saddlePointDualFunction Ψ₀ at u gives the supremum of the x-slice of Ψ₀ over P, viewed in EReal.