def SaddlePointRepresentation.IsBarrierSubproblemMinimizerSelection {P : Type u} {S : Type v} (representation : SaddlePointRepresentation P S) (w : P → S) : Prop

A function w : P → S is a barrier-subproblem minimizer selection for a saddle-point representation when each chosen point w x belongs to the canonical minimizing fiber of the saddle slice Ψ(x, ·).

theorem SaddlePointRepresentation.IsBarrierSubproblemMinimizerSelection.apply {P : Type u} {S : Type v} {representation : SaddlePointRepresentation P S} {w : P → S} (hw : representation.IsBarrierSubproblemMinimizerSelection w) (x : P) : w x ∈ constrainedArgmin Set.univ (representation.saddleFunction x)

Evaluating a barrier-subproblem minimizer selection at x yields a point of the canonical argmin set of the saddle slice Ψ(x, ·).

theorem SaddlePointRepresentation.IsBarrierSubproblemMinimizerSelection.isMinOn {P : Type u} {S : Type v} {representation : SaddlePointRepresentation P S} {w : P → S} (hw : representation.IsBarrierSubproblemMinimizerSelection w) (x : P) : IsMinOn (representation.saddleFunction x) Set.univ (w x)

The selected point w x minimizes the saddle slice Ψ(x, ·) on the whole parameter space S.

theorem SaddlePointRepresentation.IsBarrierSubproblemMinimizerSelection.objective_eq_saddleFunction {P : Type u} {S : Type v} {representation : SaddlePointRepresentation P S} {w : P → S} (hw : representation.IsBarrierSubproblemMinimizerSelection w) (x : P) : representation.objective x = representation.saddleFunction x (w x)

Along a minimizing branch, the represented objective value equals the saddle value at the selected minimizer.

def SaddlePointRepresentation.barrierSubgradientSelection {P : Type u} {S : Type v} (firstSubgradient : P → S → P) (w : P → S) : P → P

The selected field attached to Definition 7.60 sends x to the chosen first-argument saddle subgradient ∇₁Ψ(x, w(x)).

theorem SaddlePointRepresentation.barrierSubgradientSelection_apply {P : Type u} {S : Type v} (firstSubgradient : P → S → P) (w : P → S) (x : P) : barrierSubgradientSelection firstSubgradient w x = firstSubgradient x (w x)

Evaluating barrierSubgradientSelection at x returns the chosen first-argument saddle subgradient at (x, w(x)).

def SaddlePointRepresentation.IsBarrierSubgradientSelection {P : Type u} {S : Type v} [NormedAddCommGroup P] [InnerProductSpace ℝ P] (representation : SaddlePointRepresentation P S) (g : P → P) : Prop

A selected barrier subgradient field is a pointwise subgradient of the represented objective on the whole-space relative subdifferential ∂[Set.univ] representation(x).

theorem SaddlePointRepresentation.IsBarrierSubgradientSelection.apply {P : Type u} {S : Type v} [NormedAddCommGroup P] [InnerProductSpace ℝ P] {representation : SaddlePointRepresentation P S} {g : P → P} (hg : representation.IsBarrierSubgradientSelection g) (x : P) : g x ∈ subdifferentialWithin Set.univ representation.objective x

Evaluating a selected barrier subgradient field at x gives a subgradient of the represented objective at x.

theorem SaddlePointRepresentation.barrierSubgradientSelection_isBarrierSubgradientSelection {P : Type u} {S : Type v} [NormedAddCommGroup P] [InnerProductSpace ℝ P] [NormedAddCommGroup S] [InnerProductSpace ℝ S] {representation : SaddlePointRepresentation P S} {w : P → S} (hw : representation.IsBarrierSubproblemMinimizerSelection w) (saddleSubgradient : P → S → P × S) (hsub : ∀ (x : P), WithLp.toLp 2 (saddleSubgradient x (w x)) ∈ subdifferential (fun (z : WithLp 2 (P × S)) => ↑(representation.saddleFunction z.ofLp.1 z.ofLp.2)) (WithLp.toLp 2 (x, w x))) (hvar : ∀ (x : P) (y : S), inner ℝ (saddleSubgradient x (w x)).2 (y - w x) ≥ 0) : representation.IsBarrierSubgradientSelection (barrierSubgradientSelection (fun (x : P) (s : S) => (saddleSubgradient x s).1) w)

Definition 7.60: [Subgradient selection] if w(x) is a chosen minimizer of the saddle slice Ψ(x, ·) and ∇₁Ψ is a chosen subgradient with respect to the first argument, then the selected field x ↦ ∇₁Ψ(x, w(x)) is a subgradient selection of the represented objective.