DefinitionDefinition: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Saddle points of extended-real Lagrangians

Definition

Let $X, Y$ be nonempty subsets of finite-dimensional real Euclidean spaces and let $Ψ : X \times Y \to [- \infty, + \infty]$ be an extended-real function. A pair $(x_{*}, y_{*})$ is a saddle point of $Ψ$ if $Ψ (x_{*}, y_{*})$ is finite and $Ψ (x_{*}, y) \leq Ψ (x_{*}, y_{*}) \leq Ψ (x, y_{*}) (x \in X, y \in Y) .$ The inequalities must be defined at the arguments they display. For an equality-constrained problem the primal set may be a product set of finite-valued pairs $(x, z)$ .

Facts & Assumptions

Given: Nonempty subsets $X, Y$ of finite-dimensional real Euclidean spaces and an extended-real function $Ψ$ as above.

[A1]

The displayed evaluations are defined and the central value is finite.

[F1]

The extended real line $\overline{R} = R \cup {- \infty, + \infty}$ , its order, and the arithmetic that is left undefined: extended-real values are ordered in $[- \infty, + \infty]$ .

[F2]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : each finite-dimensional Euclidean space carries a real inner product and its induced norm.

Proof

1.1A1givenF1F2

The definition is a pair of quantified order inequalities with a finite central value. Only the displayed evaluations are needed, so a partial formula such as $f (x) + ⟨ K x, y ⟩ - g^{*} (y)$ is safe when each displayed saddle evaluation is defined.

2.1A1givenF1algebra∎

Restricting $X, Y$ can remove a violation of a saddle inequality, so a saddle point on the restricted sets need not be one on the original sets. For a fixed finite central value, the inequalities extend to the original sets precisely when every omitted left-hand value is at most that central value and every omitted right-hand value is at least it, with all evaluations defined. In particular, omitted $- \infty$ values on the left and $+ \infty$ values on the right cause no obstruction. No minimax interchange or existence theorem follows from this definition.

Depends on

Used by

Dependency tree · two levels

21 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Stephen Boyd and Lieven Vandenberghe, Convex Optimization, §5.1 (standard reference, not scraped)
Antonin Chambolle and Thomas Pock, A First-Order Primal-Dual Algorithm for Convex Problems with Applications to Imaging, §2 (standard reference, not scraped)