TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

PDHG has an O(1/k) ergodic saddle-gap bound

Statement

Assume the hypotheses of Chambolle–Pock primal-dual hybrid gradient and that $Φ (x, y) = f (x) + ⟨ K x, y ⟩ - g^{*} (y)$ has a saddle point $(x_{*}, y_{*})$ in the sense of Saddle points of extended-real Lagrangians. For $N \geq 1$ define ${\overset{ˉ}{x}}_{N} = \frac{1}{N} \sum_{k = 0}^{N - 1} x^{k + 1}, {\overset{ˉ}{y}}_{N} = \frac{1}{N} \sum_{k = 0}^{N - 1} y^{k + 1} .$ For every $x \in dom f$ , $y \in dom g^{*}$ , $Φ ({\overset{ˉ}{x}}_{N}, y) - Φ (x, {\overset{ˉ}{y}}_{N}) \leq \frac{1}{N} (\frac{∥ x - x^{0} ∥_{2}^{2}}{2 τ} + \frac{∥ y - y^{0} ∥_{2}^{2}}{2 σ}) .$ In particular, the saddle gap $Φ ({\overset{ˉ}{x}}_{N}, y_{*}) - Φ (x_{*}, {\overset{ˉ}{y}}_{N})$ is nonnegative and obeys this bound with $(x, y) = (x_{*}, y_{*})$ . On bounded test sets the displayed upper bound is $O (1 / N)$ . This is an ergodic gap statement; it is not a pointwise objective bound and does not assert pointwise iterate convergence.

Facts & Assumptions

Given: The exact PDHG recurrence, positive steps with $τ σ ∥ K ∥_{2}^{2} < 1$ , and a saddle point.

[A1]

The exact recurrence, strict step condition, and a saddle point hold.

[F1]

Chambolle–Pock primal-dual hybrid gradient: $f, g^{*}$ are proper closed convex and the iterates follow the exact recurrence.

[F2]

PDHG one-step primal-dual gap telescope: for every test pair and $N \geq 1$ , the sum of the first $N$ saddle differences is at most the initial weighted squared distance.

[F3]

Saddle points of extended-real Lagrangians: $Φ (x_{*}, y) \leq Φ (x_{*}, y_{*}) \leq Φ (x, y_{*})$ for all $x, y$ .

Proof

1.1A1F1givenalgebra

Every exact proximal output lies in the effective domain of its function. Convexity therefore puts ${\overset{ˉ}{x}}_{N}$ in $dom f$ and ${\overset{ˉ}{y}}_{N}$ in $dom g^{*}$ .

2.1A1F1F2step 1.1algebra

By convexity in [F1], $f ({\overset{ˉ}{x}}_{N}) \leq N^{- 1} \sum_{k < N} f (x^{k + 1})$ and $g^{*} ({\overset{ˉ}{y}}_{N}) \leq N^{- 1} \sum_{k < N} g^{*} (y^{k + 1})$ ; linearity gives $K {\overset{ˉ}{x}}_{N} = N^{- 1} \sum K x^{k + 1}$ . Hence $Φ ({\overset{ˉ}{x}}_{N}, y) - Φ (x, {\overset{ˉ}{y}}_{N}) \leq \frac{1}{N} \sum_{k = 0}^{N - 1} (Φ (x^{k + 1}, y) - Φ (x, y^{k + 1})) .$ Apply [F2] and divide by $N$ to get the bound.

3.1A1F3step 2.1∎

By the saddle inequalities [F3], $Φ ({\overset{ˉ}{x}}_{N}, y_{*}) \geq Φ (x_{*}, y_{*})$ and $Φ (x_{*}, {\overset{ˉ}{y}}_{N}) \leq Φ (x_{*}, y_{*})$ , so their difference is nonnegative. Step 2.1 at $(x_{*}, y_{*})$ supplies the same $O (1 / N)$ upper bound. The ergodic estimate makes no claim about a single nonaveraged objective difference or pointwise iterate convergence.

Depends on

Used by

A two-pixel TV denoising PDHG step in CSR form Example

Dependency tree · two levels

15 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

Antonin Chambolle and Thomas Pock, A First-Order Primal-Dual Algorithm for Convex Problems with Applications to Imaging, Theorem 1(b), §3.1 (standard reference, not scraped)
Laurent Vandenberghe, UCLA EE236C Lecture Notes: Douglas–Rachford Splitting, §§4–5 (standard reference, not scraped)