TheoremStatement: 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.

Proximal bundle accumulation under vanishing aggregate-model error

Statement

Let $F : R^{n} \to (- \infty, + \infty]$ be proper, closed, and convex. Suppose $C = dom F$ is nonempty, closed, and convex, and $F ∣_{C}$ is continuous. Consider an infinite full-memory continuation of Finite-memory-free proximal bundle method with serious and null steps with fixed $t > 0$ and $m_{s} \in (0, 1)$ , centers $x_{k} \in C$ , finite affine models $M_{k} \leq F$ on $C$ touching their centers ( $M_{k} (x_{k}) = F (x_{k})$ ), and exact candidates $z_{k} = \arg \min_{y \in C} (M_{k} (y) + \frac{∥ y - x_{k} ∥_{2}^{2}}{2 t}) .$ Assume every predicted decrease $P_{k} = F (x_{k}) - M_{k} (z_{k})$ is positive, each trial uses the stated serious/null acceptance test, the initial sublevel set $K = {x \in C : F (x) \leq F (x_{0})}$ is compact, and the aggregate-model errors $e_{k} = F (z_{k}) - M_{k} (z_{k})$ satisfy $e_{k} \to 0$ . Then every accumulation point, meaning a limit of a subsequence in the Euclidean metric, is a global minimizer of $F$ . At least one accumulation point exists. The vanishing-error premise is an additional assumption; full-memory cutting planes alone are not asserted to imply it.

Facts & Assumptions

Given: The serious/null algorithm Finite-memory-free proximal bundle method with serious and null steps, model-subproblem existence The proximal bundle model subproblem has a unique minimizer, the aggregate-error estimate Vanishing aggregate-model error controls the proximal candidate, proximal resolvent Existence, resolvent characterization, and firm nonexpansiveness of the proximal map, extended-real subgradient definition Subdifferentials of proper extended-real convex functions, compact sequential compactness In any metric space compactness implies countable compactness and limit point compactness, and each of countable compactness and limit point compactness implies sequential compactness; every implication here is proved without a choice principle, and attainment on compact metric spaces A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value.

[F1]

Each candidate is unique, and the exact proximal point $p_{k} = {prox}_{t F} (x_{k})$ exists, is unique, and the proximal map is nonexpansive (The proximal bundle model subproblem has a unique minimizer, Proximal mapping, Existence, resolvent characterization, and firm nonexpansiveness of the proximal map).

[F2]

The model error is nonnegative and $∥ z_{k} - p_{k} ∥_{2}^{2} \leq 4 t e_{k}$ (Vanishing aggregate-model error controls the proximal candidate).

[F3]

If $0 \in \partial F (x)$ , then $F (y) \geq F (x)$ for every $y$ by the extended-real subgradient definition (Subdifferentials of proper extended-real convex functions).

[F4]

A sequence is a function on the naturals, convergence is the metric limit, and every sequence in compact $K$ has a subsequence converging in $K$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ , In any metric space compactness implies countable compactness and limit point compactness, and each of countable compactness and limit point compactness implies sequential compactness; every implication here is proved without a choice principle, Open cover, subcover, compact metric space, and compact subset of a metric space). Two limits in a metric space agree (A sequence in a metric space has at most one limit). A continuous real function on compact $K$ is bounded below (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value, Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form).

Proof

1.1givenF4algebra

A serious step has $F (x_{k}) - F (z_{k}) \geq m_{s} P_{k} > 0$ ; a null step leaves the center fixed. Thus centers remain in the initial sublevel set $K$ , and $F (x_{k})$ is nonincreasing and bounded below there by [F4]. The decreases $d_{k} = F (x_{k}) - F (x_{k + 1}) \geq 0$ have bounded partial sums, since $\sum_{k < q} d_{k} = F (x_{0}) - F (x_{q})$ . If $d_{k}$ failed to tend to zero, some positive $ϵ$ would be exceeded by infinitely many terms, making these partial sums unbounded; hence $d_{k} \to 0$ .

1.2F1F2F4givenalgebra

Let $x_{k_{j}} \to \overset{ˉ}{x}$ be any accumulation subsequence, which exists for at least one subsequence by [F4]. For any chosen convergent subsequence, compactness gives a further subsequence converging to a point of $K$ ; the uniqueness-of-limits fact in [F4] identifies that point with $\overset{ˉ}{x}$ , so $\overset{ˉ}{x} \in K$ . Applying compactness to the whole center sequence also supplies at least one accumulation subsequence. By nonexpansiveness in [F1], $p_{k_{j}} = {prox}_{t F} (x_{k_{j}}) \to p = {prox}_{t F} (\overset{ˉ}{x})$ . By [F2] and $e_{k_{j}} \to 0$ , $∥ z_{k_{j}} - p_{k_{j}} ∥_{2} \to 0$ , so $z_{k_{j}} \to p$ . Since $F ∣_{C}$ is continuous and all these points lie in $C$ , $F (x_{k_{j}}) \to F (\overset{ˉ}{x})$ and $F (z_{k_{j}}) \to F (p)$ .

2.1F1F3step 1.2algebraassume-contra

Suppose for contradiction that $\overset{ˉ}{x}$ is not a global minimizer. Then $p \neq \overset{ˉ}{x}$ : otherwise the resolvent equivalence in [F1] gives $0 = (\overset{ˉ}{x} - p) / t \in \partial F (\overset{ˉ}{x})$ , and [F3] would make $\overset{ˉ}{x}$ globally minimizing. By proximal minimality, $F (p) + ∥ p - \overset{ˉ}{x} ∥_{2}^{2} / (2 t) \leq F (\overset{ˉ}{x})$ ; therefore $δ : = F (\overset{ˉ}{x}) - F (p) > 0$ .

3.1givenstep 1.1step 1.2step 2.1algebradischarge-contradiction∎

Along the chosen subsequence, $D_{j} : = F (x_{k_{j}}) - F (z_{k_{j}}) \to δ$ by step 1.2, while $P_{k_{j}} = F (x_{k_{j}}) - M_{k_{j}} (z_{k_{j}}) = D_{j} + e_{k_{j}}$ . Hence $D_{j} - m_{s} P_{k_{j}} = (1 - m_{s}) D_{j} - m_{s} e_{k_{j}} \to (1 - m_{s}) δ > 0$ . For all sufficiently large $j$ the step is serious and $d_{k_{j}} = D_{j} \geq δ / 2$ , contradicting $d_{k} \to 0$ from step 1.1. Thus every accumulation point is a global minimizer.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

92 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)