ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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.

One proximal-gradient step for a nonorthogonal Lasso design

Example

Use the Lasso objective of Lasso estimator for fixed design with $n = d = 2$ , $X = (\begin{array}{cc} 1 & 0 \\ 1 & 1 \end{array}), y = (\begin{array}{c} 1 \\ 1 \end{array}), τ = \frac{1}{10},$ and start at $θ_{0} = (0, 0)$ . The columns of $X$ have inner product $1$ , so this is not an orthogonal design. With valid smoothness constant $L = 3$ , one exact proximal-gradient update is $θ_{1} = (\frac{3}{5}, \frac{4}{15}) .$ This is a first iterate calculation; it does not claim that $θ_{1}$ minimizes the Lasso objective.

Facts & Assumptions

Given: The design, response, penalty and initial vector displayed in the Example.

[F1]

Lasso estimator for fixed design: $Q_{y} (θ) = n^{- 1} ∥ y - X θ ∥_{2}^{2} + 2 τ ∥ θ ∥_{1}$ .

[F2]

Proximal-gradient, FISTA, and fixed-period restarted FISTA: one proximal-gradient step is $θ_{1} = {prox}_{g / L} (θ_{0} - \nabla f (θ_{0}) / L)$ with $f = n^{- 1} ∥ y - X θ ∥_{2}^{2}$ and $g = 2 τ ∥ \cdot ∥_{1}$ .

[F3]

The proximal map of the l1 norm is soft thresholding: the positive multiple of $∥ \cdot ∥_{1}$ is proper, closed and convex, and its proximal map applies $S_{s λ}$ coordinatewise.

Verification

1.1F1F2F3givenalgebra

Here $f (θ) = \frac{1}{2} ∥ y - X θ ∥_{2}^{2}$ is a convex continuously differentiable quadratic: for $0 \leq α \leq 1$ , $f ((1 - α) u + α v) = (1 - α) f (u) + α f (v) - α (1 - α) ∥ X (u - v) ∥_{2}^{2} / 2.$ Its gradient is $\nabla f (θ) = H θ - X^{T} y$ with $H = X^{T} X = (\begin{array}{cc} 2 & 1 \\ 1 & 1 \end{array})$ . For $h = (a, b)$ , $∥ H h ∥_{2}^{2} = (2 a + b)^{2} + (a + b)^{2} = 5 a^{2} + 6 a b + 2 b^{2} \leq 8 a^{2} + 5 b^{2} \leq 8 ∥ h ∥_{2}^{2},$ using $6 a b \leq 3 (a^{2} + b^{2})$ . Thus $\nabla f$ is $\sqrt{8}$ -Lipschitz and $L = 3$ is valid. The nonsmooth term $g = (1 / 5) ∥ \cdot ∥_{1}$ is proper, closed and convex by [F3]. Also $X^{T} y = (2, 1)$ , so $\nabla f (θ_{0}) = (- 2, - 1)$ and $θ_{0} - \nabla f (θ_{0}) / 3 = (2 / 3, 1 / 3)$ .

2.1F2F3step 1.1algebra∎

The nonsmooth term is $g = (1 / 5) ∥ \cdot ∥_{1}$ , and the proximal parameter is $1 / 3$ , so its soft-threshold level is $(1 / 3) (1 / 5) = 1 / 15$ . Applying [F3] to $(2 / 3, 1 / 3)$ gives $(2 / 3 - 1 / 15, 1 / 3 - 1 / 15) = (3 / 5, 4 / 15)$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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

Neal Parikh and Stephen Boyd, Proximal Algorithms, §6.5.2 (standard reference, not scraped)