TheoremStatement: AI-adaptedProof: AI-generatedPipeline-generated

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 coordinate contraction from strong convexity of the composite

Statement

For a finite horizon $k$ , use an algorithm budget $K \geq k$ and do not request a proximal-gradient stopping tolerance before that horizon.

Let $B_{1}, \dots, B_{n}$ be a partition of $R^{d}$ into nonempty coordinate blocks, with $n, d \geq 1$ . Let $f : R^{d} \to R$ be convex and continuously differentiable, with positive block-gradient Lipschitz constants $L_{i}$ , and let $g (x) = \sum_{i = 1}^{n} g_{i} (x_{B_{i}})$ , where each $g_{i}$ is proper, closed and convex in the closed-epigraph convention. Set $F = f + g$ and $L_{\max} = \max_{i} L_{i} > 0$ . Assume $F$ itself is $μ$ -strongly convex for some $μ > 0$ : for finite-domain $x, y$ and $s \in [0, 1]$ , $F ((1 - s) x + s y) \leq (1 - s) F (x) + s F (y) - \frac{μ}{2} s (1 - s) ∥ x - y ∥_{2}^{2} .$ No strong convexity of $f$ alone is required, and no inequality $μ \leq L_{\max}$ is assumed.

Run Randomized proximal coordinate descent with certified inner solves from $F (x^{0}) < + \infty$ , with common majorizer $M_{i} = L_{\max}$ and uniform independent block draws. Fix a finite horizon $k$ and deterministic bounds $ϵ_{0}, \dots, ϵ_{k - 1} \geq 0$ . Assume the first $k$ updates are executed with accepted inner-model gap certificates at most $ϵ_{j}$ at every history in the finite block-history distribution; a stopping or failed call supplies no unexecuted later iterate. Then $F$ has a unique minimizer $x^{*}$ and, with $q_{c} = 1 - \frac{μ}{n (L_{\max} + μ)} \in (0, 1),$ $E [F (x^{k}) - F (x^{*})] \leq q_{c}^{k} (F (x^{0}) - F (x^{*})) + \sum_{j = 0}^{k - 1} q_{c}^{k - 1 - j} ϵ_{j} .$ The expectation is the finite weighted sum over the uniformly sampled block histories, not a distribution conditioned on successful calls. At $k = 0$ the sum is empty and the bound is equality. Exact updates have $ϵ_{j} = 0$ . This includes curvature contributed by the separable penalties; it does not assert the sharper factor $1 - μ / (n L_{\max})$ without additional smooth-part curvature.

Facts & Assumptions

Given: The functions, constants, strong-convexity segment inequality, finite initial point, sampling rule and accepted per-history updates in the Statement.

[F1]

Randomized proximal coordinate descent with certified inner solves: the selected block minimizes its quadratic model, or is accepted with certified model gap at most $ϵ_{k}$ ; other blocks stay fixed.

[F2]

Coordinate proximal subproblems are attained uniquely and descend: every exact block model has a unique minimizer and an accepted error- $ϵ_{k}$ update raises $F$ by at most $ϵ_{k}$ .

[F3]

Coordinate-block smoothness descent model: the smooth term obeys the block quadratic upper model with constant $L_{i} \leq L_{\max}$ .

[F4]

Finite separable block penalties are proper, closed, and convex: the finite separable sum $g$ is proper, closed and convex; its proof uses only closed sublevels of the block epigraphs and finite products of neighborhoods.

[F5]

A proper closed convex function has an affine minorant: a proper closed convex function on a finite-dimensional Euclidean space has an affine minorant.

[F6]

A finite continuous convex summand preserves proper closed convexity: adding finite continuous convex $f$ to $g$ preserves properness, closedness and convexity.

[F7]

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: closed bounded subsets of finite-dimensional Euclidean space are compact.

[F8]

Semicontinuous extreme value theorem on compact Euclidean sets: a real-valued lower-semicontinuous function on a nonempty compact Euclidean set attains its minimum.

[F9]

Proper closed convex extended-real functions on $R^{n}$ : properness is nonempty finite domain, convexity is the extended-real segment inequality, and closedness is closedness of the epigraph.

[F10]

Differentiable convex functions are characterized by the gradient inequality: for convex differentiable $f$ , $f (w) \geq f (x) + ⟨ \nabla f (x), w - x ⟩$ .

[F11]

Continuously differentiable maps, local inverses, and local diffeomorphisms and Total differentiability gives a local $O (∥ h ∥_{2})$ increment bound and therefore continuity: the $C^{1}$ smooth term is continuous, as required by [F6].

[F12]

The principle of mathematical induction: a recurrence bound holding at zero and preserved at successors holds for every finite horizon.

[F13]

Laws of finite sums and finite products: finite weighted sums obey additivity and scaling for averaging over block choices and histories.

[A1]

The segment strong-convexity inequality in the Statement holds for $F$ , with $μ > 0$ ; $f$ is convex and $L_{\max} > 0$ .

[A2]

Every executed history through the horizon has accepted certificates, with deterministic errors $ϵ_{j}$ ; block sampling remains independent and uniform, without conditioning on successful histories. Finite-sum laws [F13] justify averaging the conditional bounds over these histories.

Proof

1.1A1F4F5F6F7F8F9F11givenconstructalgebra

By [F4], $g$ is proper closed convex, and by [F11], $f$ is continuous. Applying [F6] makes $F$ proper closed convex. Define $H (x) = F (x) - μ ∥ x ∥_{2}^{2} / 2$ , keeping $+ \infty$ off the finite domain. It is proper. The identity $∥ (1 - s) x + s y ∥_{2}^{2} = (1 - s) ∥ x ∥_{2}^{2} + s ∥ y ∥_{2}^{2} - s (1 - s) ∥ x - y ∥_{2}^{2}$ and [A1] show $H$ is convex, including the extended-real endpoint convention. The epigraph of $H$ is the preimage of the closed epigraph of $F$ under the continuous map $(x, a) \mapsto (x, a + μ ∥ x ∥_{2}^{2} / 2)$ ; hence $H$ is closed. By [F5] applied to $H$ , $F (x) \geq μ ∥ x ∥_{2}^{2} / 2 + ⟨ a, x ⟩ + b$ for some $a, b$ , so $F$ is coercive. For a finite-domain $\overset{ˉ}{x}$ , the nonempty sublevel $S = {x : F (x) \leq F (\overset{ˉ}{x})}$ is closed by the closed epigraph and bounded by coercivity, hence compact by [F7]. The restriction $F ∣_{S}$ is real-valued and lower semicontinuous, so [F8] attains its minimum. Points outside $S$ cannot improve it. The midpoint inequality [A1] forbids distinct minimizers, giving a unique $x^{*}$ .

1.2A2F1F2F3F13givenalgebra

Fix a finite current point $x$ . For block $i$ let $z_{i}$ be the exact minimizer of $Q_{i} (u) = ⟨ \nabla_{i} f (x), u - x_{B_{i}} ⟩ + \frac{L_{\max}}{2} ∥ u - x_{B_{i}} ∥_{2}^{2} + g_{i} (u) .$ Existence and uniqueness follow from [F2]. Define $M_{x} (w) = f (x) + ⟨ \nabla f (x), w - x ⟩ + \frac{L_{\max}}{2} ∥ w - x ∥_{2}^{2} + g (w) .$ Separation of the finite block sum shows $z = (z_{i})_{i}$ minimizes $M_{x}$ , and $\sum_{i} [Q_{i} (z_{i}) - Q_{i} (x_{B_{i}})] = M_{x} (z) - F (x)$ . By [F3] and $L_{i} \leq L_{\max}$ , the actual update in a sampled block satisfies $F (x^{+}) \leq F (x) + Q_{i} (z_{i}) - Q_{i} (x_{B_{i}}) + ϵ_{j} .$ By [F13], averaging over the uniform block choice at this fixed history therefore gives $E [F (x^{+}) ∣ history] \leq F (x) + \frac{M_{x} (z) - F (x)}{n} + ϵ_{j} .$ All quantities are finite at these points because accepted model gaps and exact block minima are finite.

2.1A1F9F10step 1.1step 1.2givenalgebra

By [F10], convex differentiability of $f$ gives $f (x) + ⟨ \nabla f (x), w - x ⟩ \leq f (w)$ . Thus, for $w_{s} = (1 - s) x + s x^{*}$ , $M_{x} (w_{s}) - F (x) \leq F (w_{s}) - F (x) + \frac{L_{\max} s^{2}}{2} ∥ x^{*} - x ∥_{2}^{2} .$ These segment values are finite by convexity of the effective domain. Apply [A1] to obtain $M_{x} (z) - F (x) \leq - s (F (x) - F (x^{*})) + \frac{L_{\max} s^{2} - μ s (1 - s)}{2} ∥ x^{*} - x ∥_{2}^{2} .$ Choose $s = μ / (L_{\max} + μ) \in (0, 1)$ . The squared-distance coefficient vanishes, so $M_{x} (z) - F (x) \leq - s (F (x) - F (x^{*}))$ . This does not require $μ \leq L_{\max}$ .

3.1A2step 1.2step 2.1algebra

Substitute step 2.1 in step 1.2 to get $E [F (x^{j + 1}) - F (x^{*}) ∣ history] \leq q_{c} (F (x^{j}) - F (x^{*})) + ϵ_{j} .$ By [A2] all histories in the finite product distribution are present; summing the inequality with their weights gives $ϕ_{j + 1} \leq q_{c} ϕ_{j} + ϵ_{j}$ , where $ϕ_{j} = E [F (x^{j}) - F (x^{*})]$ . No conditioning on the event of a successful inner solve is used.

4.1F12step 2.1step 3.1algebra∎

The proposed bound at $k = 0$ is $ϕ_{0} = ϕ_{0}$ . If $ϕ_{j} \leq q_{c}^{j} ϕ_{0} + \sum_{ℓ < j} q_{c}^{j - 1 - ℓ} ϵ_{ℓ}$ , multiply by $q_{c} > 0$ and use step 3.1 to obtain the bound at $j + 1$ . By [F12], finite induction proves the displayed convolution. It specializes to exact-update contraction when every $ϵ_{j} = 0$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

83 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 J. Wright, Coordinate Descent Algorithms, §3.7 (coordinate model context; the composite-curvature variant is proved locally) (standard reference, not scraped)