Rule (3.6) gives $(1+2\gamma_k\mu_B)/\gamma_k^2 = (1-2\gamma_{k+1}\mu_C\eta)/\gamma_{k+1}^2$

Proved

ThreeOpSplitting.Accel.stepsize_identity_part1

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

accelerationp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1stepsize

Let $\mu_B \ge 0$ , $\mu_C > 0$ , $\eta \in (0,1)$ and $\gamma_0 > 0$ , and let $(\gamma_k)_{k \ge 0}$ be generated by the stepsize rule (3.6). Then for every $k \ge 0$

\frac{1 + 2\gamma_k\mu_B}{\gamma_k^2} = \frac{1 - 2\gamma_{k+1}\mu_C\eta}{\gamma_{k+1}^2}.

This identity is what the rule (3.6) is designed for: it matches the coefficient of $\|x_B^{k+1} - x^*\|^2$ on the left of (3.9), divided by $\gamma_k^2$ , with the coefficient of $\|x_B^{k+1} - x^*\|^2$ on the right of (3.9) at the next step, divided by $\gamma_{k+1}^2$ , so that (3.9) telescopes.

Preamble

import Mathlib
import Definitions.Def_ThreeOpSplitting_Accel_Stepsizes

open Filter Topology

Formal statement

namespace ThreeOpSplitting.Accel

/-- Proof of Theorem 3.3, Part 1 (p. 845): the rule (3.6) ensures
`(1 + 2γ_kμ_B)/γ_k² = (1 - 2γ_{k+1}μ_Cη)/γ_{k+1}²` for all `k ≥ 0`. -/
theorem stepsize_identity_part1 (μB μC η γ0 : ℝ)
    (hμB : 0 ≤ μB) (hμC : 0 < μC) (hη0 : 0 < η) (hη1 : η < 1) (hγ0 : 0 < γ0) (k : ℕ) :
    (1 + 2 * stepsPart1 μB μC η γ0 k * μB) / stepsPart1 μB μC η γ0 k ^ 2
      = (1 - 2 * stepsPart1 μB μC η γ0 (k + 1) * μC * η) / stepsPart1 μB μC η γ0 (k + 1) ^ 2 := by sorry

end ThreeOpSplitting.Accel

Source

Davis and Yin, A Three-Operator Splitting Scheme and its Optimization Applications, Set-Valued Var. Anal. 25 (2017), https://doi.org/10.1007/s11228-017-0421-z, p. 845, Section 3.3, proof of Theorem 3.3, Part 1 (unnumbered display)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $\mu_B, \mu_C, \eta, \gamma_0$ be real numbers with

\mu_B \ge 0,\qquad \mu_C > 0,\qquad 0 < \eta < 1,\qquad \gamma_0 > 0.

Let $(\gamma_j)$ be the sequence that starts at $\gamma_0$ and satisfies

\gamma_{j+1} = \frac{-2\gamma_j^2\mu_C\eta + \sqrt{(2\gamma_j^2\mu_C\eta)^2 + 4(1+2\gamma_j\mu_B)\gamma_j^2}}{2(1+2\gamma_j\mu_B)}.

Here the square root of a negative number is read as $0$ , and division by $0$ gives $0$ .

The theorem states that for every $k \in \mathbb{N}$ , including $k = 0$ ,

\frac{1 + 2\gamma_k\mu_B}{\gamma_k^2} = \frac{1 - 2\gamma_{k+1}\mu_C\eta}{\gamma_{k+1}^2}.

The quotients in this identity use the same convention that division by $0$ gives $0$ . If some $\gamma_{k+1}$ were $0$ , the right side would be read as $0$ , and similarly for $\gamma_k$ on the left. The statement itself does not say that the $\gamma_j$ are nonzero. For $k = 0$ the left side is $(1 + 2\gamma_0\mu_B)/\gamma_0^2$ with the given $\gamma_0 > 0$ . The case $\mu_B = 0$ is allowed.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Rule (3.6) gives (1+2γkμB)/γk2=(1−2γk+1μCη)/γk+12(1+2\gamma_k\mu_B)/\gamma_k^2 = (1-2\gamma_{k+1}\mu_C\eta)/\gamma_{k+1}^2(1+2γk​μB​)/γk2​=(1−2γk+1​μC​η)/γk+12​

Rule (3.6) gives $(1+2\gamma_k\mu_B)/\gamma_k^2 = (1-2\gamma_{k+1}\mu_C\eta)/\gamma_{k+1}^2$