LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

The proximal bundle model subproblem has a unique minimizer

Statement

Let $C \subseteq R^{n}$ be nonempty, closed, and convex; let $t > 0$ , $v \in R^{n}$ , and let $m_{i} (y) = b_{i} + ⟨ a_{i}, y ⟩$ be a nonempty finite list of affine functions. Then $Φ (y) = \max_{i} m_{i} (y) + \frac{∥ y - v ∥_{2}^{2}}{2 t}, y \in C,$ has a unique global minimizer on $C$ .

Facts & Assumptions

Given: Closed convex feasibility (A convex subset of $R^{m}$ contains every line segment between two of its points, Interior, closure, boundary, limit point, isolated point and dense subset of a metric space), the Euclidean norm and Cauchy–Schwarz (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation), closed bounded compactness (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line), and attainment on compact sets (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[F1]

A finite maximum of affine maps obeys $∣ \max_{i} m_{i} (y) - \max_{i} m_{i} (z) ∣ \leq \max_{i} ∣ m_{i} (y) - m_{i} (z) ∣$ ; each difference is $∣ ⟨ a_{i}, y - z ⟩ ∣ \leq ∥ a_{i} ∥_{2} ∥ y - z ∥_{2}$ by Cauchy–Schwarz (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation).

[F2]

The quadratic difference obeys $∣ ∥ y - v ∥_{2}^{2} - ∥ z - v ∥_{2}^{2} ∣ \leq (∥ y - v ∥_{2} + ∥ z - v ∥_{2}) ∥ y - z ∥_{2}$ , by expansion and Cauchy–Schwarz (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation).

[F3]

Continuity in a metric space is the epsilon-delta property at every point (Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form).

[F4]

$R^{0}$ consists of one vector, its zero vector (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

Proof

1.1F4givenalgebra

If $n = 0$ , [F4] says $R^{0}$ is a singleton, so the nonempty feasible set $C$ is that singleton. The finite maximum and quadratic objective have one feasible value, and its sole feasible point is the unique global minimizer. For the remainder assume $n \geq 1$ .

1.2F1F2F3givenchoose

By [F1] and [F2], $Φ$ has a finite local Lipschitz bound on $C$ around each point: the finitely many $∥ a_{i} ∥_{2}$ are bounded, and the quadratic difference in [F2] has a bounded factor on a sufficiently small ball. Hence $Φ$ is continuous on $C$ by [F3]. Choose $y_{0} \in C$ and let $c = Φ (y_{0})$ . The sublevel set $S = {y \in C : Φ (y) \leq c}$ is nonempty. If $y \in C ∖ S$ , continuity supplies an ambient ball around $y$ whose intersection with $C$ lies in $C ∖ S$ ; if $y \notin C$ , closedness of $C$ supplies a ball disjoint from $C$ . Thus every point outside $S$ has a ball disjoint from $S$ , so $S$ is closed in $R^{n}$ .

2.1givenstep 1.2algebra

The first affine cut gives $Φ (y) \geq b_{1} + ⟨ a_{1}, y ⟩ + ∥ y - v ∥_{2}^{2} / (2 t) = β + ∥ y - (v - t a_{1}) ∥_{2}^{2} / (2 t)$ , where $β = b_{1} + ⟨ a_{1}, v ⟩ - t ∥ a_{1} ∥_{2}^{2} / 2$ . Since $c = Φ (y_{0}) \geq β$ , every $y \in S$ satisfies $∥ y - (v - t a_{1}) ∥_{2}^{2} \leq 2 t (c - β)$ and thus lies in the open ball of radius $1 + \sqrt{2 t (c - β)}$ about $v - t a_{1}$ . So $S$ is bounded (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space) and compact by Heine–Borel. The continuous real-valued restriction $Φ ∣_{S}$ attains its minimum by the extreme-value theorem; points outside $S$ have value greater than $c$ , while the minimum on $S$ is at most $c$ , so this is a global minimizer.

3.1givenstep 2.1algebra∎

For every index $i$ , affinity gives $m_{i} ((p + q) / 2) = (m_{i} (p) + m_{i} (q)) / 2 \leq (\max_{j} m_{j} (p) + \max_{j} m_{j} (q)) / 2$ ; taking the finite maximum over $i$ proves the model midpoint value is at most the average endpoint values. For distinct $p, q \in C$ , the quadratic term satisfies $∥ (p + q) / 2 - v ∥_{2}^{2} = (∥ p - v ∥_{2}^{2} + ∥ q - v ∥_{2}^{2}) / 2 - ∥ p - q ∥_{2}^{2} / 4$ . After multiplication by $1 / (2 t)$ the quadratic term is strictly below the endpoint average. If both $p, q$ minimized $Φ$ , their midpoint would therefore have smaller value, a contradiction. The minimizer is unique.

Depends on

Used by

Cited to discharge well-definedness by Finite-memory-free proximal bundle method with serious and null steps.

Dependency tree · two levels

65 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

Mateo Díaz and Benjamin Grimmer, Optimal Convergence Rates for the Proximal Bundle Method, §§2–3 (standard reference, not scraped)
Dominikus Noll, Olivier Prot, and Aude Rondepierre, A proximity control algorithm to minimize nonsmooth and nonconvex functions, §§2–4 (standard reference, not scraped)